- Author:
- J. L. Krivine
No abstract available.
Cited By
- Accattoli B, Guerrieri G and Leberle M Strong Call-by-Value and Multi Types Theoretical Aspects of Computing – ICTAC 2023, (196-215)
Accattoli B, Lago U and Vanoni G The space of interaction Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science, (1-13)- Pistone P On generalized metric spaces for the simply typed lambda-calculus Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science, (1-14)
- Olimpieri F Intersection type distributors Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science, (1-15)
- Dal Lago U, de Visme M, Mazza D and Yoshimizu A (2019). Intersection types and runtime errors in the pi-calculus, Proceedings of the ACM on Programming Languages, 3:POPL, (1-29), Online publication date: 2-Jan-2019.
- Breuvart F and Lago U On Intersection Types and Probabilistic Lambda Calculi Proceedings of the 20th International Symposium on Principles and Practice of Declarative Programming, (1-13)
- Accattoli B, Graham-Lengrand S and Kesner D (2018). Tight typings and split bounds, Proceedings of the ACM on Programming Languages, 2:ICFP, (1-30), Online publication date: 30-Jul-2018.
- Vial P Every λ-Term is Meaningful for the Infinitary Relational Model Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, (899-908)
- Larchey-Wendling D Typing Total Recursive Functions in Coq Interactive Theorem Proving, (371-388)
- Vial P Infinitary intersection types as sequences Proceedings of the 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, (1-12)
- Blot V An interpretation of system F through bar recursion Proceedings of the 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, (1-12)
- Bucciarelli A, Kesner D and Ventura D (2016). Strong Normalization through Intersection Types and Memory, Electronic Notes in Theoretical Computer Science (ENTCS), 323:C, (75-91), Online publication date: 11-Jul-2016.
- Ehrhard T Call-By-Push-Value from a Linear Logic Point of View Proceedings of the 25th European Symposium on Programming Languages and Systems - Volume 9632, (202-228)
- Rahli V and Bickford M A nominal exploration of intuitionism Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs, (130-141)
- Kesner D and Ventura D A Resource Aware Computational Interpretation for Herbelin's Syntax Proceedings of the 12th International Colloquium on Theoretical Aspects of Computing - ICTAC 2015 - Volume 9399, (388-403)
- Munch-Maccagnoni G Formulae-as-types for an involutive negation Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), (1-10)
- Breuvart F On the characterization of models of H Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), (1-10)
- Manzonetto G and Tranquilli P (2012). Strong normalization of MLF via a calculus of coercions, Theoretical Computer Science, 417, (74-94), Online publication date: 1-Feb-2012.
- Santo J, Ivetić J and Likavec S (2012). Characterising Strongly Normalising Intuitionistic Terms, Fundamenta Informaticae, 121:1-4, (83-120), Online publication date: 1-Jan-2012.
- Van Bakel S, Barbanera F and De'Liguoro U A filter model for the λµ-calculus Proceedings of the 10th international conference on Typed lambda calculi and applications, (213-228)
- Lasson M Controlling program extraction in light logics Proceedings of the 10th international conference on Typed lambda calculi and applications, (123-137)
- Bernardy J and Lasson M Realizability and parametricity in pure type systems Proceedings of the 14th international conference on Foundations of software science and computational structures: part of the joint European conferences on theory and practice of software, (108-122)
- Carraro A, Ehrhard T and Salibra A Resource combinatory algebras Proceedings of the 35th international conference on Mathematical foundations of computer science, (233-245)
- Saurin A (2010). Typing streams in the Λμ-calculus, ACM Transactions on Computational Logic, 11:4, (1-34), Online publication date: 1-Jul-2010.
- Maingaud S, Balat V, Bubel R, Hähnle R and Miquel A Specifying imperative ML-like programs using dynamic logic Proceedings of the 2010 international conference on Formal verification of object-oriented software, (122-137)
- Pagani M and Rocca S (2010). Linearity, Non-determinism and Solvability, Fundamenta Informaticae, 103:1-4, (173-202), Online publication date: 1-Jan-2010.
- Pagani M and Tortora de Falco L (2010). Strong normalization property for second order linear logic, Theoretical Computer Science, 411:2, (410-444), Online publication date: 1-Jan-2010.
- Vaux L (2009). The algebraic lambda calculus, Mathematical Structures in Computer Science, 19:5, (1029-1059), Online publication date: 1-Oct-2009.
- Berline C, Manzonetto G and Salibra A (2009). Effective λ-models versus recursively enumerable λ-theories, Mathematical Structures in Computer Science, 19:5, (897-942), Online publication date: 1-Oct-2009.
- Munch-Maccagnoni G Focalisation and classical realisability Proceedings of the 23rd CSL international conference and 18th EACSL Annual conference on Computer science logic, (409-423)
- Biasi C and Aschieri F (2008). A Term Assignment for Polarized Bi-intuitionistic Logic and its Strong Normalization, Fundamenta Informaticae, 84:2, (185-205), Online publication date: 5-Sep-2008.
- Riba C Union of Reducibility Candidates for Orthogonal Constructor Rewriting Proceedings of the 4th conference on Computability in Europe: Logic and Theory of Algorithms, (498-510)
- Boudol G (2008). On strong normalization and type inference in the intersection type discipline, Theoretical Computer Science, 398:1-3, (63-81), Online publication date: 20-May-2008.
- Biasi C and Aschieri F (2008). A Term Assignment for Polarized Bi-intuitionistic Logic and its Strong Normalization, Fundamenta Informaticae, 84:2, (185-205), Online publication date: 1-Apr-2008.
- Aydemir B, Charguéraud A, Pierce B, Pollack R and Weirich S (2008). Engineering formal metatheory, ACM SIGPLAN Notices, 43:1, (3-15), Online publication date: 14-Jan-2008.
- Aydemir B, Charguéraud A, Pierce B, Pollack R and Weirich S Engineering formal metatheory Proceedings of the 35th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, (3-15)
- Miquel A Classical program extraction in the calculus of constructions Proceedings of the 21st international conference, and Proceedings of the 16th annuall conference on Computer Science Logic, (313-327)
- Boudol G Fair cooperative multithreading Proceedings of the 18th international conference on Concurrency Theory, (272-286)
- Liquori L and Ronchi Della Rocca S (2007). Intersection-types à la Church, Information and Computation, 205:9, (1371-1386), Online publication date: 1-Sep-2007.
- Vaux L (2007). The differential λμ-calculus, Theoretical Computer Science, 379:1-2, (166-209), Online publication date: 1-Jul-2007.
- Vaux L On linear combinations of λ-terms Proceedings of the 18th international conference on Term rewriting and applications, (374-388)
- Santo J, Ghilezan S and Ivetić J Characterising strongly normalising intuitionistic sequent terms Proceedings of the 2007 international conference on Types for proofs and programs, (85-99)
- Paolini L, Pimentel E and Della Rocca S An operational characterization of strong normalization Proceedings of the 9th European joint conference on Foundations of Software Science and Computation Structures, (367-381)
- Dezani-Ciancaglini M, Honsell F and Motohama Y (2005). Compositional characterisations of λ-terms using intersection types, Theoretical Computer Science, 340:3, (459-495), Online publication date: 31-Aug-2005.
- Colson L, Jonoska N and Margenstern M λP systems and typed λ-calculus Proceedings of the 5th international conference on Membrane Computing, (1-18)
- Jonoska N and Margenstern M (2004). Tree Operations in P Systems and λ-Calculus, Fundamenta Informaticae, 59:1, (67-90), Online publication date: 1-Jan-2004.
- Ehrhard T and Regnier L (2003). The differential Lambda-calculus, Theoretical Computer Science, 309:1, (1-41), Online publication date: 2-Dec-2003.
- Vestergaard R and Brotherston J (2003). A formalised first-order confluence proof for the λ-calculus using one-sorted variable names, Information and Computation, 183:2, (212-244), Online publication date: 15-Jun-2003.
- Boudol G On strong normalization in the intersection type discipline Proceedings of the 6th international conference on Typed lambda calculi and applications, (60-74)
- Jonoska N and Margenstern M (2003). Tree operations in P systems and λ-calculus, Fundamenta Informaticae, 59:1, (67-90), Online publication date: 1-Jun-2003.
- Fiore M Semantic analysis of normalisation by evaluation for typed lambda calculus Proceedings of the 4th ACM SIGPLAN international conference on Principles and practice of declarative programming, (26-37)
- Dezani-Ciancaglini M and Ghilezan S Two behavioural lambda models Proceedings of the 2002 international conference on Types for proofs and programs, (127-147)
- Dowek G Higher-order unification and matching Handbook of automated reasoning, (1009-1062)
Index Terms
- Lambda-calculus, types and models
Recommendations
A Typed Lambda Calculus with Gradual Intersection Types
PPDP '22: Proceedings of the 24th International Symposium on Principles and Practice of Declarative ProgrammingIntersection types have the power to type expressions which are all of many different types. Gradual types combine type checking at both compile-time and run-time. Here we combine these two approaches in a new typed calculus that harness both of their ...
Label dependent lambda calculus and gradual typing
Dependently-typed programming languages are gaining importance, because they can guarantee a wide range of properties at compile time. Their use in practice is often hampered because programmers have to provide very precise types. Gradual typing is a ...
Interpretations of the gradually-typed lambda calculus
Scheme '12: Proceedings of the 2012 Annual Workshop on Scheme and Functional ProgrammingGradual typing is an approach to integrating static and dynamic type checking within the same language [Siek and Taha 2006]. Given the name "gradual typing", one might think that the most interesting aspect is the type system. It turns out that the ...
Reviews
Victor W. Marek
A wealth of material concerning &lgr;-calculus and type theory is presented in 10 chapters. The first chapter covers the basics of &lgr;-calculus, including &bgr;-conversion and &eegr;-conversion. Next, the author presents the classical results on the representation of partial recursive functions in &lgr;-calculus. These include the fix-point theorems (including their counterparts in &lgr;-calculus). In the next chapter, Krivine presents the theory of Coppo and Dezani-Ciancaglini of intersection-type systems. Curry-Howard isomorphism is also treated here. Normalization theory (the existence of standard reductions for &bgr;-reducibility) is presented in chapter 4. In the next chapter, Krivine shows the fundamental result of Bo¨hm on the reduction of non-&bgr;-equivalent terms to the prescribed terms. In chapter 6, the author introduces combinatory logic, and also discusses the translation of &lgr;-calculus into combinatory logic. In chapter 7, the author studies various models of &lgr;-calculus. This chapter covers classical results of Engeler, Scott, and others. Girard's system F is studied in chapter 8. In chapter 9, the author presents his own theory of second-order functional arithmetic. Arithmetic functions (that is, elements of Baire space) definable in system F (that is, functions provably total in the system of second-order arithmetic over combinatory logic) are investigated in chapter 10. This short description of the content of the book should indicate that one can find an immense amount of information. Unfortunately, the book was written with a total disregard for the nonspecialist. In particular, a computer scientist hoping to use this book as auxiliary reading for a course in functional programming will be seriously disappointed. Excellent texts explaining the relationship of functional programming and &lgr;-calculus exist; see Barendregt [1]. An individual experienced in &lgr;-calculus will find elegant proofs and a coherent presentation in this book. For those not so fortunate as to know the &lgr;-calculus already, the book will be simply harmful. It says nothing about why the author is doing what he is doing, to what it may be applied, and what it explains. This omission is a real pity, for with some additional work, it could be an excellent text.
Access critical reviews of Computing literature here
Become a reviewer for Computing Reviews.