, The call-by-need lambda calculus, Journal of Functional Programming, vol.7, issue.3, pp.265-301, 1993.
DOI : 10.1017/S0956796897002724
, Classical Call-by-Need Sequent Calculi: The Unity of Semantic Artifacts, Proceedings of FLOPS'12. Proceedings, LNCS, pp.32-46, 2012.
DOI : 10.1007/978-3-642-29822-6_6
URL : https://hal.archives-ouvertes.fr/hal-00697241
, A Symmetric Lambda Calculus for Classical Program Extraction, Information and Computation, vol.125, issue.2, pp.103-117, 1996.
DOI : 10.1006/inco.1996.0025
, The Call-by-Need Lambda Calculus, Revisited, Programming Languages and Systems -21st European Symposium on Programming , ESOP 2012, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012. Proceedings, pp.128-147, 2012.
DOI : 10.1007/978-3-642-28869-2_7
, A confluent ??-calculus with a catch/throw mechanism, Journal of Functional Programming, vol.9, issue.6, pp.625-647, 1999.
DOI : 10.1017/S0956796899003512
URL : https://hal.archives-ouvertes.fr/hal-00094601
, The duality of computation, Proceedings of ICFP 2000, pp.233-243, 2000.
DOI : 10.1145/357766.351262
URL : https://hal.archives-ouvertes.fr/inria-00156377
, Normalization by realizability also evaluates, Proceedings of JFLA'15, 2015.
URL : https://hal.archives-ouvertes.fr/hal-01099138
, Reasoning with continuations, Proceedings of LICS'86, pp.131-141, 1986.
, On girard's 'candidats de reductibilité, Odifreddi, editor, Logic and Computer Science, pp.123-203, 1900.
, Lazy evaluation and delimited control, Logical Methods in Computer Science, vol.6, issue.3, 2010.
DOI : 10.1145/1480881.1480903
URL : http://arxiv.org/pdf/1003.5197
, Une extension d? Linterpretation de gödel a ? Lanalyse, et son application a ? Lelimination des coupures dan? Lanalyse et la theorie des types, Proceedings of the Second Scandinavian Logic Symposium, volume 63 of Studies in Logic and the Foundations of Mathematics, pp.63-92
, Specifying Peirce's law in classical realizability, Mathematical Structures in Computer Science, vol.7, issue.07, pp.1269-1303, 2016.
DOI : 10.1016/S0304-3975(02)00776-4
, Classical realizability and arithmetical formul??, Mathematical Structures in Computer Science, vol.84, issue.06, pp.1-40, 2016.
DOI : 10.1007/s001530000057
, C'est maintenant qu'on calcule: au coeur de la dualité, 2005.
, A Constructive Proof of Dependent Choice, Compatible with Classical Logic, 2012 27th Annual IEEE Symposium on Logic in Computer Science, pp.365-374, 2012.
DOI : 10.1109/LICS.2012.47
URL : https://hal.archives-ouvertes.fr/hal-00697240
, Reasoning About Call-by-need by Means of Types, pp.424-441
DOI : 10.1016/0304-3975(92)90297-S
, Lambda-calculus, types and models. Ellis Horwood series in computers and their applications, 1993.
URL : https://hal.archives-ouvertes.fr/cel-00574575
, Dependent choice, ???quote??? and the clock, Theoretical Computer Science, vol.308, issue.1-3, pp.259-276, 2003.
DOI : 10.1016/S0304-3975(02)00776-4
URL : https://hal.archives-ouvertes.fr/hal-00154478
, Realizability in classical logic In interactive models of computation and program behaviour, 2009.
, Realizability algebras: a program to well order R, Logical Methods in Computer Science, vol.40, issue.3, 2011.
DOI : 10.1007/s001530000057
URL : https://hal.archives-ouvertes.fr/hal-00483232
, Realizability algebras II : new models of ZF + DC, Logical Methods in Computer Science, vol.8, issue.1, p.10, 2012.
DOI : 10.1007/s001530000057
URL : https://hal.archives-ouvertes.fr/hal-00497587
, On the structure of classical realizability models of ZF, 2014.
, Continuations semantics or expressing implication by negation, 1993.
, Explaining the lazy krivine machine using explicit substitution and addresses. Higher-Order and Symbolic Computation, pp.257-270, 2007.
URL : https://hal.archives-ouvertes.fr/inria-00198756
, A classical realizability model for a semantical value restriction Held as Part of the European Joint Conferences on Theory and Practice of Software, Programming Languages and Systems -25th European Symposium on Programming Proceedings, volume 9632 of Lecture Notes in Computer Science, pp.476-502, 2016.
, The call-by-need lambda calculus, Journal of Functional Programming, vol.8, issue.3, pp.275-317, 1998.
DOI : 10.1017/S0956796898003037
, Existential witness extraction in classical realizability and via a negative translation 28. ´ Etienne Miquey. Classical realizability and side-effects, Logical Methods in Computer Science, vol.7, issue.2, pp.188-202, 2011.
, Focalisation and Classical Realisability, Computer Science Logic '09, pp.409-423, 2009.
DOI : 10.1016/0304-3975(87)90045-4
URL : https://hal.archives-ouvertes.fr/inria-00409793
, Call-by-need and continuationpassing style, Lisp and Symbolic Computation, pp.57-82, 1994.
DOI : 10.1007/bf01019945
URL : http://www-cgi.cs.cmu.edu/afs/cs.cmu.edu/project/fox/mosaic/papers/petel-lazy-p.ps
, Free deduction: An analysis of ???Computations??? in classical logic, Proceedings of LPAR, pp.361-380, 1991.
DOI : 10.1007/3-540-55460-2_27
, Strong normalization of second order symmetric lambda-calculus Foundations of Software Technology and Theoretical Computer Science, Proceedings, pp.442-453, 1974.
, Classical By-Need, Programming Languages and Systems: 25th European Symposium on Programming , ESOP 2016, Proceedings, pp.616-643, 2016.
DOI : 10.1017/S0956796898003141
, Call-by-name, call-by-value and the ??-calculus, Theoretical Computer Science, vol.1, issue.2, pp.125-159, 1975.
DOI : 10.1016/0304-3975(75)90017-1
, Strong normalization of lambda-mu-mu/tilde-calculus with explicit substitutions, Foundations of Software Science and Computation Structures 7th International Conference, FOSSACS 2004, Held as Part of the Joint European Conferences on Theory and Practice of Software Proceedings, volume 2987 of Lecture Notes in Computer Science, pp.423-437, 2004.
, Intensional interpretations of functionals of finite type i, Journal of Symbolic Logic, vol.32, issue.2, pp.198-212, 1967.