×

Journal of Functional Programming

Short Title: J. Funct. Program.
Publisher: Cambridge University Press, Cambridge
ISSN: 0956-7968; 1469-7653/e
Online: https://www.cambridge.org/core/journals/journal-of-functional-programming/all-issues
Comments: Journal; Indexed cover-to-cover
Documents Indexed: 632 Publications (since 1991)
References Indexed: 338 Publications with 10,428 References.
all top 5

Latest Issues

33 (2023)
32 (2022)
31 (2021)
30 (2020)
29 (2019)
28 (2018)
27 (2017)
26 (2016)
25 (2015)
24, No. 6 (2014)
24, No. 5 (2014)
24, No. 4 (2014)
24, No. 2-3 (2014)
24, No. 1 (2014)
23, No. 6 (2013)
23, No. 5 (2013)
23, No. 4 (2013)
23, No. 3 (2013)
23, No. 2 (2013)
23, No. 1 (2013)
22, No. 6 (2012)
22, No. 4-5 (2012)
22, No. 3 (2012)
22, No. 2 (2012)
22, No. 1 (2012)
21, No. 6 (2011)
21, No. 4-5 (2011)
21, No. 3 (2011)
21, No. 2 (2011)
21, No. 1 (2011)
20, No. 5-6 (2010)
20, No. 3-4 (2010)
20, No. 2 (2010)
20, No. 1 (2010)
19, No. 6 (2009)
19, No. 5 (2009)
19, No. 3-4 (2009)
19, No. 2 (2009)
19, No. 1 (2009)
19, Suppl. (2009)
18, No. 5-6 (2008)
18, No. 4 (2008)
18, No. 3 (2008)
18, No. 2 (2008)
18, No. 1 (2008)
17, No. 6 (2007)
17, No. 4-5 (2007)
17, No. 3 (2007)
17, No. 2 (2007)
17, No. 1 (2007)
16, No. 6 (2006)
16, No. 4-5 (2006)
16, No. 3 (2006)
16, No. 2 (2006)
16, No. 1 (2006)
15, No. 6 (2005)
15, No. 5 (2005)
15, No. 4 (2005)
15, No. 3 (2005)
15, No. 2 (2005)
15, No. 1 (2005)
14, No. 6 (2004)
14, No. 5 (2004)
14, No. 3 (2004)
14, No. 2 (2004)
14, No. 1 (2004)
13, No. 6 (2003)
13, No. 5 (2003)
13, No. 4 (2003)
13, No. 3 (2003)
13, No. 2 (2003)
13, No. 1 (2003)
12, No. 6 (2002)
12, No. 4-5 (2002)
12, No. 3 (2002)
12, No. 2 (2002)
12, No. 1 (2002)
11, No. 6 (2001)
11, No. 5 (2001)
11, No. 4 (2001)
11, No. 3 (2001)
11, No. 2 (2001)
11, No. 1 (2001)
10, No. 6 (2000)
10, No. 5 (2000)
10, No. 4 (2000)
10, No. 3 (2000)
10, No. 2 (2000)
10, No. 1 (2000)
9, No. 6 (1999)
9, No. 5 (1999)
9, No. 4 (1999)
9, No. 3 (1999)
9, No. 2 (1999)
9, No. 1 (1999)
8, No. 6 (1998)
8, No. 5 (1998)
8, No. 4 (1998)
8, No. 3 (1998)
8, No. 2 (1998)
...and 26 more Volumes
all top 5

Authors

18 Bird, Richard S.
18 Hinze, Ralf
13 Hutton, Graham
13 Peyton Jones, Simon L.
11 Danvy, Olivier
10 Weirich, Stephanie
9 Dreyer, Derek R.
9 Erwig, Martin
9 Pierce, Benjamin C.
8 Abel, Andreas M.
8 Findler, Robert Bruce
8 McBride, Conor Thomas
7 Gibbons, Jeremy
7 Harper, Robert
7 Morrisett, Greg
7 Mu, Shin-Cheng
7 Swierstra, Wouter
7 Wadler, Philip Lee
6 Barendregt, Hendrik Pieter
6 Jansson, Patrik
6 Sabry, Amr
5 Acar, Umut A.
5 Ariola, Zena M.
5 Barthe, Gilles
5 Claessen, Koen
5 Crary, Karl
5 Curtis, Sharon A.
5 Devriese, Dominique
5 Fluet, Matthew T.
5 Gordon, Andrew D.
5 Kiselyov, Oleg
5 Might, Matthew
5 Okasaki, Chris
5 Oliveira, Bruno C.d. S.
5 Palsberg, Jens
5 Runciman, Colin
5 Schrijvers, Tom
5 Thiemann, Peter J.
5 VanHorn, David A.
5 Vytiniotis, Dimitrios
4 Atkey, Robert
4 Bierman, Gavin M.
4 Birkedal, Lars
4 Breitner, Joachim
4 Burton, F. Warren
4 Cardelli, Luca
4 de Moor, Oege
4 Felleisen, Matthias
4 Flatt, Matthew
4 Hu, Zhenjiang
4 Kamareddine, Fairouz D.
4 Kennedy, Andrew J.
4 Licata, Daniel R.
4 Marlow, Simon
4 Nanevski, Aleksandar
4 Nipkow, Tobias
4 Owens, Scott
4 Paterson, Ross A.
4 Pientka, Brigitte
4 Sulzmann, Martin
4 Wakeling, David
3 Abadi, Martín
3 Achten, Peter
3 Altenkirch, Thorsten
3 Bahr, Patrick
3 Benton, Nick
3 Bernardy, Jean-Philippe
3 Botta, Nicola
3 Cockx, Jesper
3 Coquand, Thierry
3 Curien, Pierre-Louis
3 Dagand, Pierre-Evariste
3 Downen, Paul
3 Ghani, Neil
3 Henglein, Fritz
3 Herbelin, Hugo
3 Huet, Gerard P.
3 Jaskelioff, Mauro
3 Jay, C. Barry
3 Jeuring, Johan
3 Johann, Patricia
3 Jones, Mark P.
3 Jones, Neil D.
3 Leroy, Xavier
3 Lescanne, Pierre
3 Lindley, Sam
3 Mairson, Harry George
3 Maranget, Luc
3 Moggi, Eugenio
3 Morihata, Akimasa
3 New, Max S.
3 Pfenning, Frank
3 Piessens, Frank
3 Pottier, François
3 Pretnar, Matija
3 Rainey, Mike
3 Reppy, John H.
3 Rossberg, Andreas
3 Sergey, Ilya
3 Serrano, Manuel
...and 715 more Authors

Publications by Year

Citations contained in zbMATH Open

441 Publications have been cited 3,040 times in 1,951 Documents Cited by Year
Special issue: Haskell 98 language and librairies. The revised report. Zbl 1067.68041
129
2003
Explicit substitutions. Zbl 0941.68542
Abadi, Martin; Cardelli, Luca; Curien, P.-L.; Lévy, J.-J.
124
1991
Applicative programming with effects. Zbl 1128.68020
McBride, Conor; Paterson, Ross
51
2008
Linear type theory for asynchronous session types. Zbl 1185.68194
Gay, Simon J.; Vasconcelos, Vasco T.
44
2010
The Zipper. Zbl 0893.68014
Huet, Gérard
43
1997
Propositions as sessions. Zbl 1307.68025
Wadler, Philip
41
2014
Introduction to generalized type systems. Zbl 0931.03019
Barendregt, Henk
34
1991
The view from the left. Zbl 1069.68539
McBride, Conor; McKinna, James
32
2004
de Bruijn notation as a nested datatype. Zbl 0926.68025
Bird, Richard S.; Paterson, Ross
31
1999
A foundation for actor computation. Zbl 0870.68091
Agha, Gul A.; Mason, Ian A.; Smith, Scott F.; Talcott, Carolyn L.
31
1997
Classical logic, continuation semantics and abstract machines. Zbl 0928.68074
Streicher, Th.; Reus, B.
30
1998
Iris from the ground up: a modular foundation for higher-order concurrent separation logic. Zbl 1476.68062
Jung, Ralf; Krebbers, Robbert; Jourdan, Jacques-Henri; Bizjak, Aleš; Birkedal, Lars; Dreyer, Derek
30
2018
Deriving a lazy abstract machine. Zbl 0881.68049
Sestoft, Peter
29
1997
Setoids in type theory. Zbl 1060.03030
Barthe, Gilles; Capretta, Venanzio; Pons, Olivier
28
2003
\(\lambda\nu\), a calculus of explicit substitutions which preserves strong normalisation. Zbl 0873.68108
Benaissa, Zine-El-Abidine; Briaud, Daniel; Lescanne, Pierre; Rouyer-Degli, Jocelyne
28
1996
Theoretical pearls: Representing ‘undefined’ in lambda calculus. Zbl 0816.03007
Barendregt, Henk
26
1992
The call-by-need lambda calculus. Zbl 0887.68007
Ariola, Zena M.; Felleisen, Matthias
26
1997
Equivalence in functional languages with effects. Zbl 0941.68540
Mason, Ian; Talcott, Carolyn
25
1991
Efficient self-interpretation in lambda calculus. Zbl 0817.68051
Mogensen, Torben Æ.
25
1992
Idris, a general-purpose dependently typed programming language: design and implementation. Zbl 1295.68059
Brady, Edwin
25
2013
The call-by-need lambda calculus. Zbl 0918.03019
Maraist, John; Odersky, Martin; Wadler, Philip
24
1998
Algorithms with polynomial interpretation termination proof. Zbl 0987.68042
Bonfante, G.; Cichon, A.; Marion, J.-Y.; Touzet, H.
23
2001
Computational types from a logical perspective. Zbl 0920.03023
Benton, P. N.; Bierman, G. M.; de Paiva, V. C. V.
23
1998
The virtues of eta-expansion. Zbl 0833.68072
Jay, C. Barry; Ghani, Neil
22
1995
Indexed containers. Zbl 1420.68032
Altenkirch, Thorsten; Ghani, Neil; Hancock, Peter; Mcbride, Conor; Morris, Peter
22
2015
The expressive power of higher-order types or, life without CONS. Zbl 0988.68046
Jones, Neil D.
21
2001
Errata to: “Stack-based typed assembly language”. Zbl 1110.68361
Morrisett, Greg; Crary, Karl; Glew, Neal; Walker, David
21
2003
Modularity of strong normalization in the algebraic-\(\lambda\)-cube. Zbl 0918.03010
Barbanera, Franco; Fernández, Maribel; Geuvers, Herman
20
1997
Higher-order narrowing with definitional trees. Zbl 0926.68028
Hanus, Michael; Prehofer, Christian
20
1999
A positive supercompiler. Zbl 0870.68040
Sørensen, M. H.; Glück, R.; Jones, N. D.
20
1996
Data types à la carte. Zbl 1153.68015
Swierstra, Wouter
20
2008
A semantic basis for Quest. Zbl 0941.68528
Cardelli, Luca; Longo, Giuseppe
19
1991
Transformation techniques for context-sensitive rewrite systems. Zbl 1104.68056
Giesl, Jürgen; Middeldorp, Aart
19
2004
Simple type-theoretic foundations for object-oriented programming. Zbl 0817.68052
Pierce, Benjamin C.; Turner, David N.
19
1994
Regular-expression derivatives re-examined. Zbl 1163.68317
Owens, Scott; Reppy, John; Turon, Aaron
19
2009
Implementing lazy functional languages on stock hardware: the Spineless Tagless G-machine. Zbl 1159.68389
Peyton Jones, Simon L.
19
1992
Correspondence assertions for process synchronization in concurrent communications. Zbl 1077.68605
Bonelli, Eduardo; Compagnoni, Andriana; Gunter, Elsa
19
2005
Polymorphic type, region and effect inference. Zbl 0817.68099
Talpin, Jean-Pierre; Jouvelot, Pierre
18
1992
Residual theory in \(\lambda\)-calculus: A formal development. Zbl 0826.03008
Huet, Gérard
18
1994
Ott: effective tool support for the working semanticist. Zbl 1185.68201
Sewell, Peter; Nardelli, Francesco Zappa; Owens, Scott; Peskine, Gilles; Ridge, Thomas; Sarkar, Susmit; Strniša, Rok
17
2010
FUNCTIONAL PEARL: Enumerating the rationals. Zbl 1103.68444
Gibbons, Jeremy; Lester, David; Bird, Richard
17
2006
Hoare type theory, polymorphism and separation. Zbl 1155.68354
Nanevski, Aleksandar; Morrisett, Greg; Birkedal, Lars
17
2008
Self-interpretation in lambda calculus. Zbl 1159.03304
Barendregt, Henk
16
1991
A coherence theorem for Martin-Löf’s type theory. Zbl 0917.03028
Hedberg, Michael
16
1998
Parameterised notions of computation. Zbl 1191.68156
Atkey, Robert
16
2009
Categorical semantics for arrows. Zbl 1191.68406
Jacobs, Bart; Heunen, Chris; Hasuo, Ichiro
16
2009
Finally tagless, partially evaluated: tagless staged interpreters for simpler typed languages. Zbl 1191.68158
Carette, Jacques; Kiselyov, Oleg; Shan, Chung-Chieh
16
2009
Cubical Agda: a dependently typed programming language with univalence and higher inductive types. Zbl 1512.68058
Vezzosi, Andrea; Mörtberg, Anders; Abel, Andreas
16
2021
A paradigmatic object-oriented programming language: Design, static typing and semantics. Zbl 0817.68037
Bruce, Kim B.
15
1994
On characterizations of the basic feasible functionals. I. Zbl 0992.68020
Irwin, Robert J.; Royer, James S.; Kapron, Bruce M.
15
2001
Probabilistic functional programming in Haskell. Zbl 1091.68023
Erwig, Martin; Kollmansberger, Steve
15
2006
Mechanizing metatheory in a logical framework. Zbl 1125.68029
Harper, Robert; Licata, Daniel R.
14
2007
Type inference with simple subtypes. Zbl 0941.68541
Mitchell, John C.
14
1991
Practical type inference for arbitrary-rank types. Zbl 1107.68030
Jones, Simon Peyton; Vytiniotis, Dimitrios; Weirich, Stephanie; Shields, Mark
14
2007
Grammatical framework. A type-theoretical grammar formalism. Zbl 1085.68026
Ranta, Aarne
14
2004
First-class patterns. Zbl 1163.68315
Jay, Barry; Kesner, Delia
14
2009
Well-founded recursion with copatterns and sized types. Zbl 1420.68031
Abel, Andreas; Pientka, Brigitte
14
2016
Proofs for free. Parametricity for dependent types. Zbl 1271.68076
Bernardy, Jean-Philippe; Jansson, Patrik; Paterson, Ross
14
2012
Domain-free pure type systems. Zbl 0979.03013
Barthe, Gilles; Sørensen, Morten Heine
13
2000
Verification of non-functional programs using interpretations in type theory. Zbl 1111.68389
Filliâtre, Jean-Christophe
13
2003
On bunched typing. Zbl 1056.03013
O’Hearn, Peter
13
2003
Proof-producing translation of higher-order logic into pure and stateful ML. Zbl 1297.68053
Myreen, Magnus O.; Owens, Scott
13
2014
A simple library implementation of binary sessions. Zbl 1418.68036
Padovani, Luca
13
2017
Counting and generating lambda terms. Zbl 1311.68045
Grygiel, Katarzyna; Lescanne, Pierre
13
2013
A type- and scope-safe universe of syntaxes with binding: their semantics and proofs. Zbl 1522.68118
Allais, Guillaume; Atkey, Robert; Chapman, James; McBride, Conor; McKinna, James
13
2021
HOLCF=HOL+LCF. Zbl 0933.03028
Müller, Olaf; Nipkow, Tobias; von Oheimb, David; Slotosch, Oscar
12
1999
A partial evaluator for the untyped lambda-calculus. Zbl 1155.68350
Gomard, Carsten K.; Jones, Neil D.
12
1991
Dynamic typing in polymorphic languages. Zbl 0819.68142
Abadi, Martin; Cardelli, Luca; Pierce, B.; Rémy, D.
12
1995
Generalizing generalized tries. Zbl 0965.68016
Hinze, Ralf
12
2000
Lambda terms for natural deduction, sequent calculus and cut elimination. Zbl 0949.03055
Barendregt, Henk; Ghilezan, Silvia
12
2000
Algorithm + strategy = parallelism. Zbl 0933.68033
Trinder, P. W.; Hammond, K.; Loidl, H.-W.; Payton Jones, S. L.
12
1998
Parallel functional programming in Eden. Zbl 1096.68018
Loogen, Rita; Ortega-Mallén, Yolanda; Peña-Marí, Ricardo
12
2005
Finger trees: a simple general-purpose data structure. Zbl 1088.68041
Hinze, Ralf; Paterson, Ross
12
2006
Deciding validity in a spatial logic for trees. Zbl 1083.68021
Calcagno, Cristiano; Cardelli, Luca; Gordon, Andrew D.
12
2005
A monadic framework for delimited continuations. Zbl 1130.68038
Dyvbig, R. Kent; Jones, Simon Peyton; Sabry, Amr
12
2007
Recursive subtyping revealed. Zbl 1025.68017
Gapeyev, Vladimir; Levin, Michael Y.; Pierce, Benjamin C.
12
2002
Safety of Nöcker’s strictness analysis. Zbl 1153.68012
Schmidt-Schauss, Manfred; Sabel, David; Schütz, Marko
12
2008
The verified CakeML compiler backend. Zbl 1493.68091
Kiam Tan, Yong; Myreen, Magnus O.; Kumar, Ramana; Fox, Anthony; Owens, Scott; Norrish, Michael
12
2019
Effekt: capability-passing style for type- and effect-safe, extensible effect handlers in Scala. Zbl 1442.68024
Brachthäuser, Jonathan Immanuel; Schuster, Philipp; Ostermann, Klaus
12
2020
Modular proof of strong normalization for the calculus of constructions. Zbl 1159.03311
Geuvers, Herman; Nederhof, Mark-Jan
11
1991
A tutorial on the universality and expressiveness of fold. Zbl 0948.68036
Hutton, Graham
11
1999
Functional runtime systems within the lambda-sigma calculus. Zbl 0918.03018
Hardin, Thérèse; Maranget, Luc; Pagano, Bruno
11
1998
A predicative analysis of structural recursion. Zbl 0998.68027
Abel, Andreas; Altenkirch, Thorsten
11
2002
DrScheme: A programming environment for scheme. Zbl 0987.68610
Findler, Robert Bruce; Clements, John; Flanagan, Cormac; Flatt, Matthew; Krishnamurthi, Shriram; Steckler, Paul; Felleisen, Matthias
11
2002
The lambda calculus is algebraic. Zbl 1040.68023
Selinger, Peter
11
2002
Types and trace effects of higher order programs. Zbl 1142.68020
Skalka, Christian; Smith, Scott; van Horn, David
10
2008
Higher-order functions for parsing. Zbl 0817.68097
Hutton, Graham
10
1992
Understanding functional dependencies via constraint handling rules. Zbl 1107.68031
Sulzmann, Martin; Duck, Gregory J.; Peyton-Jones, Simon; Stuckey, Peter J.
10
2007
Monadic parsing in Haskell. Zbl 0917.68039
Hutton, Graham; Meijer, Erik
10
1998
Stack-based access control and secure information flow. Zbl 1077.68569
Banerjee, Anindya; Naumann, David A.
10
2005
Extending a \(\lambda\)-calculus with explicit substitution which preserves strong normalisation into a confluent calculus on open terms. Zbl 0882.03011
Kamareddine, Fairouz; Ríos, Alejandro
10
1997
The impact of higher-order state and control effects on local relational reasoning. Zbl 1252.68187
Dreyer, Derek; Neis, Georg; Birkedal, Lars
10
2012
OutsideIn(X): modular type inference with local assumptions. Zbl 1262.68034
Vytiniotis, Dimitrios; Jones, Simon Peyton; Schrijvers, Tom; Sulzmann, Martin
10
2011
Using types as search keys in function libraries. Zbl 1155.68452
Rittri, Mikael
9
1991
Promoting rewriting to a programming language: A compiler for non-deterministic rewrite programs in associative-commutative theories. Zbl 0979.68055
Kirchner, Hélène; Moreau, Pierre-Etienne
9
2001
The semantics of future and an application. Zbl 0926.68075
Flanagan, C.; Felleisen, M.
9
1999
Gabriel-Ulmer duality and Lawvere theories enriched over a general base. Zbl 1191.68163
Lack, Stephen; Power, John
9
2009
Big-step normalisation. Zbl 1191.68153
Altenkirch, Thorsten; Chapman, James
9
2009
Algebra of programming in Agda: dependent types for relational program derivation. Zbl 1191.68195
Mu, Shin-Cheng; Ko, Hsiang-Shang; Jansson, Patrik
9
2009
Consistency of the theory of contexts. Zbl 1092.68022
Bucalo, Anna; Honsell, Furio; Miculan, Marino; Scagnetto, Ivan; Hoffman, Martin
9
2006
Is sized typing for coq practical? Zbl 07697869
Chan, Jonathan; Li, Yufeng; Bowman, William J.
1
2023
Migrating gradual types. Zbl 1511.68051
Campora, John Peter III; Chen, Sheng; Erwig, Martin; Walkingshaw, Eric
2
2022
Back to futures. Zbl 07492705
Pruiksma, Klaas; Pfenning, Frank
2
2022
Fold-unfold lemmas for reasoning about recursive programs using the Coq proof assistant. Zbl 1511.68052
Danvy, Olivier
1
2022
Cubical Agda: a dependently typed programming language with univalence and higher inductive types. Zbl 1512.68058
Vezzosi, Andrea; Mörtberg, Anders; Abel, Andreas
16
2021
A type- and scope-safe universe of syntaxes with binding: their semantics and proofs. Zbl 1522.68118
Allais, Guillaume; Atkey, Robert; Chapman, James; McBride, Conor; McKinna, James
13
2021
Linear capabilities for fully abstract compilation of separation-logic-verified code. Zbl 1522.68138
Van Strydonck, Thomas; Piessens, Frank; Devriese, Dominique
3
2021
Blame and coercion: together again for the first time. Zbl 1522.68130
Siek, Jeremy G.; Thiemann, Peter; Wadler, Philip
3
2021
StkTokens: enforcing well-bracketed control flow and stack encapsulation using linear capabilities. Zbl 1522.68164
Skorstengaard, Lau; Devriese, Dominique; Birkedal, Lars
2
2021
Explainable dynamic programming. Zbl 1522.68122
Erwig, Martin; Kumar, Prashant
2
2021
Ready, set, verify! Applying hs-to-coq to real-world Haskell code. Zbl 1522.68121
Breitner, Joachim; Spector-Zabusky, Antal; Li, Yao; Rizkallah, Christine; Wiegley, John; Cohen, Joshua; Weirich, Stephanie
2
2021
Gradual type theory. Zbl 1522.68127
New, Max S.; Licata, Daniel R.; Ahmed, Amal
2
2021
Cogent: uniqueness types and certifying compilation. Zbl 1522.68128
O’Connor, Liam; Chen, Zilin; Rizkallah, Christine; Jackson, Vincent; Amani, Sidney; Klein, Gerwin; Murray, Toby; Sewell, Thomas; Keller, Gabriele
2
2021
On the correctness of monadic backward induction. Zbl 1522.68120
Brede, Nuria; Botta, Nicola
2
2021
A trustful monad for axiomatic reasoning with probability and nondeterminism. Zbl 1493.03004
Affeldt, Reynald; Garrigue, Jacques; Nowak, David; Saikawa, Takafumi
2
2021
Lambda calculus with algebraic simplification for reduction parallelisation: extended study. Zbl 1522.68126
Morihata, Akimasa
1
2021
Not by equations alone. Reasoning with extensible effects. Zbl 1522.68124
Kiselyov, Oleg; Mu, Shin-Cheng; Sabry, Amr
1
2021
Extensional equality preservation and verified generic programming. Zbl 1522.68119
Botta, Nicola; Brede, Nuria; Jansson, Patrik; Richter, Tim
1
2021
Taming the merge operator. Zbl 1519.68049
Huang, Xuejing; Zhao, Jinxu; Oliveira, Bruno C. d. S.
1
2021
Effekt: capability-passing style for type- and effect-safe, extensible effect handlers in Scala. Zbl 1442.68024
Brachthäuser, Jonathan Immanuel; Schuster, Philipp; Ostermann, Klaus
12
2020
Tight typings and split bounds, fully developed. Zbl 1482.68077
Accattoli, Beniamino; Graham-Lengrand, Stéphane; Kesner, Delia
8
2020
Effect handlers via generalised continuations. Zbl 1442.68028
Hillerström, Daniel; Lindley, Sam; Atkey, Robert
7
2020
Doo bee doo bee doo. Zbl 1442.68026
Convent, Lukas; Lindley, Sam; McBride, Conor; McLaughlin, Craig
6
2020
Local algebraic effect theories. Zbl 1482.68091
Lukšič, Žiga; Pretnar, Matija
1
2020
Explicit effect subtyping. Zbl 1482.68081
Karachalias, Georgios; Pretnar, Matija; Saleh, Amr Hany; Vanderhallen, Stien; Schrijvers, Tom
1
2020
Elaborating dependent (co)pattern matching: no pattern left behind. Zbl 1442.68025
Cockx, Jesper; Abel, Andreas
1
2020
Heterogeneous binary random-access lists. Zbl 1442.68032
Swierstra, Wouter
1
2020
Build systems à la carte: theory and practice. Zbl 1442.68029
Mokhov, Andrey; Mitchell, Neil; Peyton Jones, Simon
1
2020
The verified CakeML compiler backend. Zbl 1493.68091
Kiam Tan, Yong; Myreen, Magnus O.; Kumar, Ramana; Fox, Anthony; Owens, Scott; Norrish, Michael
12
2019
POPLMark reloaded: mechanizing proofs by logical relations. Zbl 1442.68257
Abel, Andreas; Allais, Guillaume; Hameer, Aliya; Pientka, Brigitte; Momigliano, Alberto; Schäfer, Steven; Stark, Kathrin
8
2019
How to evaluate the performance of gradual type systems. Zbl 1493.68087
Greenman, Ben; Takikawa, Asumu; New, Max S.; Feltey, Daniel; Findler, Robert Bruce; Vitek, Jan; Felleisen, Matthias
4
2019
How to prove decidability of equational theories with second-order computation analyser SOL. Zbl 1442.68027
Hamana, Makoto
3
2019
Folding left and right over Peano numbers. Zbl 1493.68084
Danvy, Olivier
2
2019
Constructive Galois connections. Zbl 1493.68104
Darais, David; Van Horn, David
1
2019
Iris from the ground up: a modular foundation for higher-order concurrent separation logic. Zbl 1476.68062
Jung, Ralf; Krebbers, Robbert; Jourdan, Jacques-Henri; Bizjak, Aleš; Birkedal, Lars; Dreyer, Derek
30
2018
The adequacy of Launchbury’s natural semantics for lazy evaluation. Zbl 1478.68137
Breitner, Joachim
3
2018
Foundations of dependent interoperability. Zbl 1476.68051
Dagand, Pierre-Évariste; Tabareau, Nicolas; Tanter, Éric
2
2018
Size-based termination of higher-order rewriting. Zbl 1476.68048
Blanqui, Frédéric
2
2018
An extended account of contract monitoring strategies as patterns of communication. Zbl 1476.68055
Swords, Cameron; Sabry, Amr; Tobin-Hochstadt, Sam
1
2018
Abstract allocation as a unified approach to polyvariance in control-flow analyses. Zbl 1476.68054
Gilray, Thomas; Adams, Michael D.; Might, Matthew
1
2018
A simple library implementation of binary sessions. Zbl 1418.68036
Padovani, Luca
13
2017
Algebraic data integration. Zbl 1475.68069
Schultz, Patrick; Wisnesky, Ryan
6
2017
Notions of computation as monoids. Zbl 1476.68098
Rivas, Exequiel; Jaskelioff, Mauro
6
2017
Quick specifications for the busy programmer. Zbl 1418.68037
Smallbone, Nicholas; Johansson, Moa; Claessen, Koen; Algehed, Maximilian
4
2017
No value restriction is needed for algebraic effects and handlers. Zbl 1418.68034
Kammar, Ohad; Pretnar, Matija
4
2017
The calculus of dependent lambda eliminations. Zbl 1418.68038
Stump, Aaron
4
2017
Programming with ornaments. Zbl 1418.68035
Ko, Hsiang-Shang; Gibbons, Jeremy
3
2017
Backtracking with cut via a distributive law and left-zero monoids. Zbl 1418.68063
Piróg, Maciej; Staton, Sam
3
2017
Normal-order reduction grammars. Zbl 1418.68111
Bendkowski, Maciej
2
2017
Contributions to a computational theory of policy advice and avoidability. Zbl 1476.68049
Botta, Nicola; Jansson, Patrik; Ionescu, Cezar
2
2017
Higher order symbolic execution for contract verification and refutation. Zbl 1418.68061
Nguyên, Phúc C.; Tobin-Hochstadt, Sam; Van Horn, David
1
2017
Interactive programming in Agda – objects and graphical user interfaces. Zbl 1418.68031
Abel, Andreas; Adelsberger, Stephan; Setzer, Anton
1
2017
The essence of ornaments. Zbl 1418.68032
Dagand, Pierre-Evariste
1
2017
A comprehensible guide to a new unifier for CIC including universe polymorphism and overloading. Zbl 1418.68185
Ziliani, Beta; Sozeau, Matthieu
1
2017
Finiteness and rational sequences, constructively. Zbl 1418.68069
Uustalu, Tarmo; Veltri, Niccolò
1
2017
Editorial: Special issue on programming with dependent types. Zbl 1418.68006
1
2017
An algebra for distributed big data analytics. Zbl 1475.68327
Fegaras, Leonidas
1
2017
Compiling a 50-year journey. Zbl 1476.68058
Hutton, Graham; Bahr, Patrick
1
2017
Well-founded recursion with copatterns and sized types. Zbl 1420.68031
Abel, Andreas; Pientka, Brigitte
14
2016
Linear lambda terms as invariants of rooted trivalent maps. Zbl 1420.68050
Zeilberger, Noam
7
2016
Efficiency of lambda-encodings in total type theory. Zbl 1420.68045
Stump, Aaron; Fu, Peng
3
2016
Homotopical patch theory. Zbl 1420.68060
Angiuli, Carlo; Morehouse, Edward; Licata, Daniel R.; Harper, Robert
3
2016
Transparent fault tolerance for scalable functional computation. Zbl 1420.68026
Stewart, Robert; Maier, Patrick; Trinder, Phil
2
2016
A characterization of lambda-terms transforming numerals. Zbl 1420.68042
Parys, Paweł
2
2016
Safe zero-cost coercions for Haskell. Zbl 1420.68035
Breitner, Joachim; Eisenberg, Richard A.; Peyton Jones, Simon; Weirich, Stephanie
2
2016
Composable scheduler activations for Haskell. Zbl 1420.68057
Sivaramakrishnan, K. C.; Harris, Tim; Marlow, Simon; Peyton Jones, Simon
1
2016
Gradual type-and-effect systems. Zbl 1420.68033
Bañados Schwerter, Felipe; Garcia, Ronald; Tanter, Éric
1
2016
Eliminating dependent pattern matching without K. Zbl 1419.68037
Cockx, Jesper; Devriese, Dominique; Piessens, Frank
1
2016
Reasoning about multi-stage programs. Zbl 1420.68040
Inoue, Jun; Taha, Walid
1
2016
Unifying structured recursion schemes. An extended study. Zbl 1420.68039
Hinze, Ralf; Wu, Nicolas
1
2016
Indexed containers. Zbl 1420.68032
Altenkirch, Thorsten; Ghani, Neil; Hancock, Peter; Mcbride, Conor; Morris, Peter
22
2015
Formalisation in higher-order logic and code generation to functional languages of the Gauss-Jordan algorithm. Zbl 1420.68185
Aransay, Jesús; Divasón, Jose
9
2015
Counting and generating terms in the binary lambda calculus. Zbl 1419.68039
Grygiel, Katarzyna; Lescanne, Pierre
7
2015
Calculating correct compilers. Zbl 1420.68053
Bahr, Patrick; Hutton, Graham
5
2015
Type-based amortized resource analysis with integers and arrays. Zbl 1420.68068
Hoffmann, Jan; Shao, Zhong
4
2015
Mtac: a monad for typed tactic programming in Coq. Zbl 1420.68189
Ziliani, Beta; Dreyer, Derek; Krishnaswami, Neelakantan R.; Nanevski, Aleksandar; Vafeiadis, Viktor
3
2015
A representation theorem for second-order functionals. Zbl 1420.68041
Jaskelioff, Mauro; O’Connor, Russell
2
2015
Interleaving data and effects. Zbl 1419.68036
Atkey, Robert; Johann, Patricia
2
2015
Teaching types with a cognitively effective worked example format. Zbl 1420.68047
Tirronen, Ville; Isomöttönen, Ville
1
2015
Generating constrained random data with uniform distribution. Zbl 1420.68036
Claessen, Koen; Duregård, Jonas; Pałka, Michał H.
1
2015
Understanding beginners’ mistakes with Haskell. Zbl 1420.68048
Tirronen, Ville; Uusi-Mäkelä, Samuel; Isomöttönen, Ville
1
2015
Verified decision procedures for MSO on words based on derivatives of regular expressions. Zbl 1420.68049
Traytel, Dmitriy; Nipkow, Tobias
1
2015
Propositions as sessions. Zbl 1307.68025
Wadler, Philip
41
2014
Proof-producing translation of higher-order logic into pure and stateful ML. Zbl 1297.68053
Myreen, Magnus O.; Owens, Scott
13
2014
Elaborating intersection and union types. Zbl 1297.68049
Dunfield, Joshua
7
2014
F-ing modules. Zbl 1322.68048
Rossberg, Andreas; Russo, Claudio; Dreyer, Derek
7
2014
Transporting functions across ornaments. Zbl 1297.68047
Dagand, Pierre-Évariste; McBride, Conor
5
2014
Delimited control and computational effects. Zbl 1297.68048
Downen, Paul; Ariola, Zena M.
2
2014
Book review of: J. van Eijck and C. Unger, Computational semantics with functional programming. Zbl 1305.00056
Orchard, Dominic
2
2014
On the complexity of stream equality. Zbl 1297.68050
Endrullis, Jörg; Hendriks, Dimitri; Bakhshi, Rena; Roşu, Grigore
1
2014
Pushdown flow analysis with abstract garbage collection. Zbl 1297.68051
Johnson, J. Ian; Sergey, Ilya; Earl, Christopher; Might, Matthew; van Horn, David
1
2014
Idris, a general-purpose dependently typed programming language: design and implementation. Zbl 1295.68059
Brady, Edwin
25
2013
Counting and generating lambda terms. Zbl 1311.68045
Grygiel, Katarzyna; Lescanne, Pierre
13
2013
Secure distributed programming with value-dependent types. Zbl 1290.68033
Swamy, Nikhil; Chen, Juan; Fournet, Cédric; Strub, Pierre-Yves; Bhargavan, Karthikeyan; Yang, Jean
8
2013
An insider’s look at LF type reconstruction: everything you (n)ever wanted to know. Zbl 1262.68030
Pientka, Brigitte
6
2013
How to make ad hoc proof automation less ad hoc. Zbl 1314.68281
Gonthier, Georges; Ziliani, Beta; Nanevski, Aleksandar; Dreyer, Derek
5
2013
Enhancing semantic bidirectionalization via shape bidirectionalizer plug-ins. Zbl 1303.68039
Voigtländer, Janis; Hu, Zhenjiang; Matsuda, Kazutaka; Wang, Meng
5
2013
Syntactic soundness proof of a type-and-capability system with hidden state. Zbl 1262.68031
Pottier, François
3
2013
Modular verification of preemptive OS kernels. Zbl 1311.68043
Gotsman, Alexey; Yang, Hongseok
1
2013
A library for polymorphic dynamic typing. Zbl 1286.68036
Swierstra, Wouter; Van Noort, Thomas
1
2013
...and 341 more Documents
all top 5

Cited by 2,224 Authors

19 Kesner, Delia
19 Yoshida, Nobuko
18 Danvy, Olivier
18 Kamareddine, Fairouz D.
17 Birkedal, Lars
17 Pfenning, Frank
15 Lucas, Salvador
15 Schmidt-Schauß, Manfred
15 Schrijvers, Tom
14 Abel, Andreas M.
14 Ghani, Neil
13 Kiselyov, Oleg
13 Thiemann, Peter J.
12 Hinze, Ralf
12 Myreen, Magnus O.
12 Nipkow, Tobias
12 Pientka, Brigitte
12 Swierstra, Wouter
12 Zucca, Elena
11 Atkey, Robert
11 Ayala-Rincón, Mauricio
11 Dezani-Ciancaglini, Mariangiola
11 Fernández, Maribel
11 Pérez, Jorge A.
11 Sabel, David
11 Uustalu, Tarmo
10 Gibbons, Jeremy
10 Goncharov, Sergeĭ Savost’yanovich
10 Schröder, Lutz
10 Talcott, Carolyn L.
10 Wadler, Philip Lee
9 Alpuente, María
9 Curien, Pierre-Louis
9 Dal Lago, Ugo
9 Geuvers, Jan Herman
9 Ghelli, Giorgio
9 Hanus, Michael
9 Harper, Robert
9 Hutton, Graham
9 McBride, Conor Thomas
9 Oliveira, Bruno C.d. S.
9 Shan, Chung-chieh
9 Stump, Aaron
9 Voigtlander, Janis
8 Accattoli, Beniamino
8 Altenkirch, Thorsten
8 Alves, Sandra
8 Ancona, Davide
8 Barthe, Gilles
8 Bizjak, Aleš
8 Blanqui, Frédéric
8 Cheney, James
8 Florido, Mário
8 Gordon, Andrew D.
8 Hamana, Makoto
8 Jouannaud, Jean-Pierre
8 Klop, Jan Willem
8 Lescanne, Pierre
8 Liquori, Luigi
8 Matthes, Ralph
8 Meseguer Guaita, José
8 Nordvall Forsberg, Fredrik
8 Peyton Jones, Simon L.
8 Pitts, Andrew M.
8 Sulzmann, Martin
8 Vasconcelos, Vasco Thudichum
8 Weirich, Stephanie
7 Barbanera, Franco
7 Bonelli, Eduardo
7 Caires, Luís
7 Di Cosmo, Roberto
7 Fujita, Ken-etsu
7 Jansson, Patrik
7 Johann, Patricia
7 Kameyama, Yukiyoshi
7 Leroy, Xavier
7 Lindley, Sam
7 Lochbihler, Andreas
7 Mackie, Ian
7 Manzonetto, Giulio
7 Møgelberg, Rasmus Ejlers
7 Moser, Georg
7 Nederpelt, Rob
7 Pym, David J.
7 Sabry, Amr
7 Smolka, Gert
7 van Bakel, Steffen
7 Lima Ventura, Daniel
7 Vidal, Germán
7 Wu, Nicolas
6 Antoy, Sergio
6 Ariola, Zena M.
6 Barendregt, Hendrik Pieter
6 Bucciarelli, Antonio
6 Caballero, Rafael E.
6 Carbone, Marco
6 Coquand, Thierry
6 Cavalcanti de Moura, Flávio Leonardo
6 Devriese, Dominique
6 Fischer, Sebastian
...and 2,124 more Authors
all top 5

Cited in 123 Journals

213 Journal of Functional Programming
169 Theoretical Computer Science
90 Information and Computation
79 Logical Methods in Computer Science
71 MSCS. Mathematical Structures in Computer Science
68 Journal of Automated Reasoning
58 Higher-Order and Symbolic Computation
37 Journal of Logical and Algebraic Methods in Programming
29 Science of Computer Programming
27 Annals of Pure and Applied Logic
25 The Journal of Logic and Algebraic Programming
22 Information Processing Letters
16 Formal Aspects of Computing
16 Theory and Practice of Logic Programming
15 Acta Informatica
12 Journal of Applied Logic
11 Journal of Symbolic Computation
10 Theory of Computing Systems
8 RAIRO. Theoretical Informatics and Applications
8 Computer Languages, Systems & Structures
7 New Generation Computing
6 Journal of Pure and Applied Algebra
6 The Journal of Symbolic Logic
6 Archive for Mathematical Logic
6 Formal Methods in System Design
6 Journal of Logic, Language and Information
6 ACM Transactions on Computational Logic
5 Journal of Computer and System Sciences
5 Indagationes Mathematicae. New Series
5 The Bulletin of Symbolic Logic
5 Annals of Mathematics and Artificial Intelligence
4 Journal of Philosophical Logic
4 Programming and Computer Software
4 Journal of Computer Science and Technology
4 International Journal of Foundations of Computer Science
4 Applied Categorical Structures
4 Fundamenta Informaticae
4 International Journal of Number Theory
3 Computers and Fluids
3 Studia Logica
3 Distributed Computing
3 Applicable Algebra in Engineering, Communication and Computing
3 Journal of Applied Non-Classical Logics
3 The Electronic Journal of Combinatorics
3 Constraints
3 Science China. Information Sciences
3 RAIRO. Theoretical Informatics and Applications
2 Discrete Applied Mathematics
2 Advances in Mathematics
2 Information Sciences
2 Notre Dame Journal of Formal Logic
2 Synthese
2 European Journal of Combinatorics
2 International Journal of Parallel Programming
2 International Journal of Approximate Reasoning
2 Elemente der Mathematik
2 RAIRO. Informatique Théorique et Applications
2 Journal of Mathematical Sciences (New York)
2 Journal of Difference Equations and Applications
2 Topoi
2 Annals of Combinatorics
2 Mathematics in Computer Science
2 Logica Universalis
1 Artificial Intelligence
1 Computer Physics Communications
1 International Journal of Mathematical Education in Science and Technology
1 Journal of Computational Physics
1 Mathematical Proceedings of the Cambridge Philosophical Society
1 Physica A
1 Chaos, Solitons and Fractals
1 Applied Mathematics and Computation
1 The Fibonacci Quarterly
1 Fuzzy Sets and Systems
1 Journal of Computational and Applied Mathematics
1 Journal of the London Mathematical Society. Second Series
1 Kodai Mathematical Journal
1 Mathematics and Computers in Simulation
1 Publications of the Research Institute for Mathematical Sciences, Kyoto University
1 Advances in Applied Mathematics
1 History and Philosophy of Logic
1 Discrete & Computational Geometry
1 Journal of Cryptology
1 Multidimensional Systems and Signal Processing
1 Real-Time Systems
1 European Journal of Operational Research
1 SIAM Review
1 Celestial Mechanics and Dynamical Astronomy
1 Cybernetics and Systems Analysis
1 Applied and Computational Harmonic Analysis
1 Bulletin des Sciences Mathématiques
1 Theory and Applications of Categories
1 ACM Transactions on Modeling and Computer Simulation
1 Mathematical Problems in Engineering
1 Parallel Algorithms and Applications
1 Journal of Automata, Languages and Combinatorics
1 European Series in Applied and Industrial Mathematics (ESAIM): Control, Optimization and Calculus of Variations
1 Journal of the ACM
1 Wuhan University Journal of Natural Sciences (WUJNS)
1 LMS Journal of Computation and Mathematics
1 Logic and Logical Philosophy
...and 23 more Journals
all top 5

Cited in 42 Fields

1,683 Computer science (68-XX)
686 Mathematical logic and foundations (03-XX)
120 Category theory; homological algebra (18-XX)
34 Combinatorics (05-XX)
19 Number theory (11-XX)
14 Algebraic topology (55-XX)
13 Information and communication theory, circuits (94-XX)
12 Order, lattices, ordered algebraic structures (06-XX)
11 Game theory, economics, finance, and other social and behavioral sciences (91-XX)
10 Quantum theory (81-XX)
8 Linear and multilinear algebra; matrix theory (15-XX)
7 Mathematics education (97-XX)
6 General algebraic systems (08-XX)
6 Group theory and generalizations (20-XX)
6 Operations research, mathematical programming (90-XX)
5 History and biography (01-XX)
5 Fluid mechanics (76-XX)
4 Probability theory and stochastic processes (60-XX)
4 Statistics (62-XX)
4 Numerical analysis (65-XX)
4 Biology and other natural sciences (92-XX)
4 Systems theory; control (93-XX)
3 General and overarching topics; collections (00-XX)
3 Commutative algebra (13-XX)
3 Difference and functional equations (39-XX)
3 Convex and discrete geometry (52-XX)
2 Measure and integration (28-XX)
2 Geometry (51-XX)
2 General topology (54-XX)
1 Field theory and polynomials (12-XX)
1 Algebraic geometry (14-XX)
1 \(K\)-theory (19-XX)
1 Topological groups, Lie groups (22-XX)
1 Special functions (33-XX)
1 Ordinary differential equations (34-XX)
1 Harmonic analysis on Euclidean spaces (42-XX)
1 Differential geometry (53-XX)
1 Manifolds and cell complexes (57-XX)
1 Mechanics of particles and systems (70-XX)
1 Mechanics of deformable solids (74-XX)
1 Classical thermodynamics, heat transfer (80-XX)
1 Statistical mechanics, structure of matter (82-XX)

Citations by Year