,
,
,
If ? ? V : A | ?; ? then: (1) c : (?,a : A, ? ? ? ?; ? ) ? c ,
,
,
,
,
Dependent Types and Fibred Computational Effects, pp.36-54 ,
, , 2016.
A type-theoretic foundation of delimited continuations, Higher-Order and Symbolic Computation, vol.22, issue.3, pp.233-273, 2009. ,
URL : https://hal.archives-ouvertes.fr/inria-00177326
A symmetric lambda calculus for classical program extraction, Inf. Comput, vol.125, issue.2, pp.103-117, 1996. ,
CPS translations and applications: The cube and beyond. Higher-Order and Symbolic Computation, vol.12, pp.125-170, 1999. ,
Hybrid realizability for intuitionistic and classical choice, LICS 2016, 2016. ,
URL : https://hal.archives-ouvertes.fr/hal-01766881
Inductively defined types, pp.50-66, 1990. ,
The duality of computation, Proceedings of ICFP 2000, vol.35, pp.233-243, 2000. ,
URL : https://hal.archives-ouvertes.fr/inria-00156377
Sequent calculus as a compiler intermediate language, ICFP 2016, 2016. ,
On various negative translations, Proceedings Third International Workshop on Classical Logic and Computation, CL&C 2010, vol.47, pp.21-33, 2010. ,
Representing monads, Proceedings of the Twenty-First Annual ACM Symposium on Principles of Programming Languages, pp.446-457, 1994. ,
Pure type systems with explicit substitutions, J. Funct. Program, vol.25, 2015. ,
Classically and intuitionistically provably recursive functions, pp.21-27, 1978. ,
Direct models for the computational lambda calculus, Electr. Notes Theor. Comput. Sci, vol.20, pp.245-292, 1999. ,
Relaxing the value restriction, Functional and Logic Programming, 7th International Symposium, vol.2998, pp.196-213, 2004. ,
A formulae-as-type notion of control, Proceedings of the 17th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '90, pp.47-58, 1990. ,
Polymorphic type assignment and CPS conversion, LISP and Symbolic Computation, vol.6, issue.3, pp.361-379, 1993. ,
On the degeneracy of sigma-types in presence of computational classical logic, Proceedings of TLCA 2005, vol.3461, pp.209-220, 2005. ,
A constructive proof of dependent choice, compatible with classical logic, Proceedings of the 27th ,
URL : https://hal.archives-ouvertes.fr/hal-00697240
, Annual IEEE Symposium on Logic in Computer Science, LICS 2012, pp.365-374, 2012.
An approach to call-by-name delimited continuations, Proceedings of the 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp.383-394, 2008. ,
URL : https://hal.archives-ouvertes.fr/inria-00524949
Short proofs of normalization for the simply-typed ?-calculus, permutative conversions and gödel's t. Archive for Mathematical Logic, vol.42, pp.59-87, 2003. ,
Realizability in classical logic, interactive models of computation and program behaviour. Panoramas et synthèses, vol.27, pp.197-229, 2009. ,
URL : https://hal.archives-ouvertes.fr/hal-00154500
A classical realizability model for a semantical value restriction, Held as Part of the European Joint Conferences on Theory and Practice of Software, vol.9632, pp.476-502, 2016. ,
URL : https://hal.archives-ouvertes.fr/hal-01107429
Semantics and Implementation of an Extension of ML for Proving Programs, 2017. ,
URL : https://hal.archives-ouvertes.fr/tel-01682908
Constructive mathematics and computer programming, Proc. Of a Discussion Meeting of the Royal Society of London on Mathematical Logic and Programming Languages, pp.167-184, 1985. ,
Existential witness extraction in classical realizability and via a negative translation, Logical Methods in Computer Science, vol.7, issue.2, 2011. ,
URL : https://hal.archives-ouvertes.fr/hal-00800560
A classical sequent calculus with dependent types, Held as Part of the European Joint Conferences on Theory and Practice of Software, pp.777-803, 2017. ,
URL : https://hal.archives-ouvertes.fr/hal-01744359
Realizability interpretation and normalization of typed call-by-need ?-calculus with control, Foundations of Software Science and Computation Structures: 21th International Conference, FOSSACS 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, 2018. ,
URL : https://hal.archives-ouvertes.fr/hal-01624839
A sequent calculus with dependent types for classical arithmetic, Proceedings of the 33nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), 2018. ,
URL : https://hal.archives-ouvertes.fr/hal-01703526
Focalisation and Classical Realisability, Computer Science Logic '09, vol.5771, pp.409-423, 2009. ,
URL : https://hal.archives-ouvertes.fr/inria-00409793
Models of a Non-associative Composition, pp.396-410, 2014. ,
URL : https://hal.archives-ouvertes.fr/hal-00996729
Proofs of strong normalisation for second order classical natural deduction, J. Symb. Log, vol.62, issue.4, pp.1461-1479, 1997. ,
Extracting F ? 's programs from proofs in the calculus of constructions, Proceedings of the 16th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '89, pp.89-104, 1989. ,
An Effectful Way to Eliminate Addiction to Dependence, Logic in Computer Science (LICS), 2017 32nd Annual ACM/IEEE Symposium, vol.12, 2017. ,
Strong normalization of lambda-bar-mu-mu-tilde-calculus with explicit substitutions, FOSSACS, vol.2987, pp.423-437, 2004. ,
URL : https://hal.archives-ouvertes.fr/hal-00004321
A framework for dependent types and effects, 2015. ,
, Search of Effectful Dependent Types, 2017.
Comparing cubes of typed and type assignment systems, Annals of Pure and Applied Logic, vol.86, issue.3, pp.267-303, 1997. ,
Call-by-value is dual to call-by-name, Proceedings of the Eighth ACM SIGPLAN International Conference on Functional Programming, pp.189-201, 2003. ,
Simple imperative polymorphism, LISP and Symbolic Computation, pp.343-356, 1995. ,