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