Dependent Types and Fibred Computational Effects, 19th International Conference on Foundations of Software Science and Computation Structures, vol.36, 2016. ,
CPS Translations and Applications: The Cube and Beyond, Higher Order Symbol. Comput, vol.12, pp.125-170, 1999. ,
Realizability and Parametricity in Pure Type Systems, Foundations of Software Science and Computational Structures, vol.6604, pp.108-122, 2011. ,
URL : https://hal.archives-ouvertes.fr/hal-00589893
Interactive Theorem Proving and Program Development, 2004. ,
URL : https://hal.archives-ouvertes.fr/hal-00344237
The next 700 syntactical models of type theory, Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, 2017. ,
URL : https://hal.archives-ouvertes.fr/hal-01445835
Type-Preserving CPS Translation of ? and ? Types is Not Not Possible, Proceedings of the 45st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL '18, 2018. ,
URL : https://hal.archives-ouvertes.fr/hal-01672735
Idris, a general-purpose dependently typed programming language: Design and implementation, Journal of Functional Programming, vol.23, pp.552-593, 2013. ,
Ready, Set, Verify! Applying hs-to-coq to Real-World Haskell Code (Experience Report), Proceedings of the ACM on Programming Languages, vol.2, p.16, 2018. ,
Combining Proofs and Programs in a Dependently Typed Language, Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2014. ,
Effective Interactive Proofs for Higher-order Imperative Programs, Proceedings of the 14th ACM SIGPLAN International Conference on Functional Programming (ICFP '09), 2009. ,
Sprinkles of Extensionality for Your Vanilla Type Theory, 22nd International Conference on Types for Proofs and Programs, 2016. ,
The Calculus of Constructions, Inf. Comput, vol.76, issue.3, pp.90005-90008, 1988. ,
URL : https://hal.archives-ouvertes.fr/inria-00076024
The Definitional Side of the Forcing, Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '16, 2016. ,
URL : https://hal.archives-ouvertes.fr/hal-01319066
CakeML: A Verified Implementation of ML, Principles of Programming Languages (POPL), pp.179-191, 2014. ,
CompCert ? A Formally Verified Optimizing Compiler, ERTS 2016: Embedded Real Time Software and Systems. SEE, 2016. ,
URL : https://hal.archives-ouvertes.fr/hal-01238879
Programmation fonctionnelle certifiée : l'extraction de programmes dans l'assistant Coq, 2004. ,
Call-by-push-value, 2001. ,
, Mathematical Components, 2008.
, Notions of Computation and Monads. Information and Computation, vol.93, issue.1, 1991.
Hoare type theory, polymorphism and separation, Journal of Functional Programming, vol.18, pp.5-6, 2008. ,
, Dependently Typed Programming in Agda, Advanced Functional Programming, vol.5832, pp.230-266, 2008.
An effectful way to eliminate addiction to dependence, 32nd Annual Symposium on Logic in Computer Science, LICS 2017, 2017. ,
Failure is Not an Option -An Exceptional Type Theory, Proceedings of the 27th European Symposium on Programming Languages and Systems, vol.10801, pp.245-271, 2018. ,
, The Coq Proof Assistant Reference Manual, 2019.
Types, Abstraction and Parametric Polymorphism, 1983. ,
,
First-Class Type Classes, Proceedings of the 21st International Conference on Theorem Proving in Higher-Order Logics, pp.278-293, 2008. ,
URL : https://hal.archives-ouvertes.fr/inria-00628864
Dependent Types and Multi-Monadic Effects in F*, 43nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL). ACM, 256?270, 2016. ,
URL : https://hal.archives-ouvertes.fr/hal-01265793
Gradual Certified Programming in Coq, Proceedings of the 11th ACM Dynamic Languages Symposium, pp.26-40, 2015. ,
URL : https://hal.archives-ouvertes.fr/hal-01238774
, Univalent Foundations Project. 2013. Homotopy Type Theory: Univalent Foundations for Mathematics
A Framework for Dependent Types and Effects, 2015. ,
Pollack-inconsistency, Proceedings of the 9th International Workshop On User Interfaces for Theorem Provers (UITP10), vol.285, 2012. ,
Dependent Types in Practical Programming, Proceedings of the 26th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL '99, pp.214-227, 1999. ,