Distilling abstract machines, Proceedings of the 19th ACM SIGPLAN International Conference on Functional Programming, pp.363-376, 2014. ,
Environments and the Complexity of Abstract Machines, The 19th International Symposium on Principles and Practice of Declarative Programming, 2017. ,
URL : https://hal.archives-ouvertes.fr/hal-01675358
,
Compiling with Continuations, 1992. ,
The call-by-need lambda calculus, J. Funct. Program, vol.7, issue.3, pp.265-301, 1993. ,
Classical call-byneed sequent calculi: The unity of semantic artifacts, Functional and Logic Programming-11th International Symposium, FLOPS 2012, pp.32-46, 2012. ,
Foundations of strong call by need, Proc. ACM Program. Lang. 1(ICFP), vol.20, 2017. ,
URL : https://hal.archives-ouvertes.fr/hal-01766206
,
An interpretation of system f through bar recursion, 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pp.1-12, 2017. ,
URL : https://hal.archives-ouvertes.fr/hal-01766883
Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the church-rosser theorem, Indagationes Mathematicae (Proceedings), vol.75, issue.5, pp.381-392, 1972. ,
,
An extension of system F with subtyping, pp.750-770, 1991. ,
Strongly reducing variants of the krivine abstract machine, Higher-Order and Symbolic Computation, vol.20, issue.3, pp.209-230, 2007. ,
,
The duality of computation, Proceedings of ICFP, vol.35, pp.233-243, 2000. ,
URL : https://hal.archives-ouvertes.fr/inria-00156377
,
Defunctionalized Interpreters for Callby-Need Evaluation, pp.240-256, 2010. ,
Control operators, the SECD-machine, and the lambda-calculus, 3rd Working Conference on the Formal Description of Programming Concepts, 1986. ,
Continuations in programming practice: Introduction and survey, 1999. ,
A syntactic theory of sequential control, Theor. Comput. Sci, vol.52, issue.3, pp.90109-90114, 1987. ,
A formulae-as-type notion of control, Proceedings of the 17th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp.47-58, 1990. ,
A constructive proof of dependent choice, compatible with classical logic, Proceedings of the 27th Annual IEEE Symposium on Logic in Computer Science, LICS 2012, pp.365-374, 2012. ,
URL : https://hal.archives-ouvertes.fr/hal-00697240
The definitional side of the forcing, Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, pp.367-376, 2016. ,
URL : https://hal.archives-ouvertes.fr/hal-01319066
Extending type theory with forcing, Proceedings of the 2012 27th Annual IEEE/ACM Symposium on Logic in Computer Science, pp.395-404, 2012. ,
URL : https://hal.archives-ouvertes.fr/hal-00685150
Reasoning About Call-by-need by Means of Types, pp.424-441, 2016. ,
Semantical considerations on modal logic, Acta Philosophica Fennica, vol.16, pp.83-94, 1963. ,
A call-by-name lambda-calculus machine, Higher Order and Symbolic Computation, 2004. ,
URL : https://hal.archives-ouvertes.fr/hal-00154508
Realizability algebras: a program to well order r, Logical Methods in Computer Science, vol.7, issue.3, 2011. ,
URL : https://hal.archives-ouvertes.fr/hal-00483232
The mechanical evaluation of expressions, The Computer Journal, vol.6, issue.4, pp.308-320, 1964. ,
Explaining the lazy krivine machine using explicit substitution and addresses, Higher-Order and Symbolic Computation, vol.20, issue.3, pp.257-270, 2007. ,
URL : https://hal.archives-ouvertes.fr/inria-00198756
The ZINC experiment: an economical implementation of the ML language, Technical report, vol.117, 1990. ,
URL : https://hal.archives-ouvertes.fr/inria-00070049
, Sheaves in Geometry and Logic, 1992.
The call-by-need lambda calculus, J. Funct. Program, vol.8, issue.3, pp.275-317, 1998. ,
Local States in String Diagrams, pp.334-348, 2014. ,
Forcing as a program transformation, LICS. pp, pp.197-206, 2011. ,
URL : https://hal.archives-ouvertes.fr/hal-00800558
A sequent calculus with dependent types for classical arithmetic, Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, pp.720-729, 2018. ,
URL : https://hal.archives-ouvertes.fr/hal-01703526
Realizability Interpretation and Normalization of Typed Call-by-Need ?-calculus With Control, FOSSACS 18-21st International Conference on Foundations of Software Science and Computation Structures. Thessalonique, 2018. ,
URL : https://hal.archives-ouvertes.fr/hal-01624839
, Topos theory, 2007.
Extracting constructive content from classical proofs, 1990. ,
Call-by-need and continuationpassing style, Lisp and Symbolic Computation, vol.7, pp.57-82, 1994. ,
,
Proofs of strong normalisation for second order classical natural deduction, J. Symb. Log, vol.62, issue.4, pp.1461-1479, 1997. ,
Notions of Computation Determine Monads, pp.342-356, 2002. ,
Call-by-name, call-by-value and the lambda-calculus, Theor. Comput. Sci, vol.1, issue.2, pp.90017-90018, 1975. ,
Deriving a lazy abstract machine, J. Funct. Program, vol.7, issue.3, pp.231-264, 1997. ,
An interpreter for extended lambda calculus, Massachusetts Institute of Technology, 1975. ,
,
,
, The proof is very similar (and easier) than the proof in the call-by-need case, by induction on typing derivations, If ? ? ? then ? ? ? : ? Proof