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 all top 5 Fields 619 Computer science (68-XX) 89 Mathematical logic and foundations (03-XX) 19 General and overarching topics; collections (00-XX) 10 Category theory; homological algebra (18-XX) 5 Combinatorics (05-XX) 5 Number theory (11-XX) 4 Mathematics education (97-XX) 3 Algebraic topology (55-XX) 3 Numerical analysis (65-XX) 3 Game theory, economics, finance, and other social and behavioral sciences (91-XX) 2 General algebraic systems (08-XX) 2 Operations research, mathematical programming (90-XX) 2 Information and communication theory, circuits (94-XX) 1 History and biography (01-XX) 1 Order, lattices, ordered algebraic structures (06-XX) 1 Mechanics of deformable solids (74-XX) 1 Quantum theory (81-XX) Publications by Year all cited Publications top 5 cited Publications 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 cited Publications top 5 cited Publications 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