Idris, a general-purpose dependently typed programming language: Design and implementation, Journal of Functional Programming, vol.36, issue.05, pp.552-593, 2013. ,
DOI : 10.1017/S0956796803004829
Programming and reasoning with algebraic effects and dependent types, ACM SIGPLAN International Conference on Functional Programming, ICFP'13, pp.133-144, 2013. ,
Resource-Dependent Algebraic Effects, Trends in Functional Programming, pp.18-33, 2015. ,
DOI : 10.1007/978-3-319-14675-1_2
A simple model for programming the web, Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015, pp.153-165, 2015. ,
The calculus of constructions, Information and Computation, vol.76, issue.2-3, 1986. ,
DOI : 10.1016/0890-5401(88)90005-3
URL : https://hal.archives-ouvertes.fr/inria-00076024
A Tactic Language for the System Coq, Logic for Programming and Automated Reasoning, 7th International Conference Proceedings, pp.85-95, 1955. ,
DOI : 10.1007/3-540-44404-1_7
URL : https://hal.archives-ouvertes.fr/hal-01125070
Dependent Types for Safe and Secure Web Programming, Proceedings of the 25th symposium on Implementation and Application of Functional Languages, IFL '13, p.49, 2013. ,
DOI : 10.1145/2620678.2620683
An axiomatic basis for computer programming, Communications of the ACM, vol.12, issue.10, pp.576-580, 1969. ,
DOI : 10.1145/363235.363259
Report on the Programming Language Haskell, A Non-strict Purely Functional Language (Version 1.2), ACM SIGPLAN Notices, vol.27, issue.5, 1992. ,
Object-oriented software engineering -a use case driven approach, 1992. ,
Tackling the awkward squad: monadic input/output , concurrency, exceptions, and foreign-language calls in haskell, Engineering theories of software construction, pp.47-96, 2001. ,
Formal verification of a realistic compiler, Communications of the ACM, vol.52, issue.7, pp.107-115, 2009. ,
DOI : 10.1145/1538788.1538814
URL : https://hal.archives-ouvertes.fr/inria-00415861
Extraction in Coq: An Overview, Proceedings, pp.359-369, 2008. ,
DOI : 10.1007/978-3-540-69407-6_39
URL : https://hal.archives-ouvertes.fr/hal-00338973
Trace-based verification of imperative programs with I/O, Journal of Symbolic Computation, vol.46, issue.2, pp.95-118, 2011. ,
DOI : 10.1016/j.jsc.2010.08.004
The Temporal Logic of Reactive and Concurrent Systems, 1992. ,
DOI : 10.1007/978-1-4612-0931-7
A theory of type polymorphism in programming, Journal of Computer and System Sciences, vol.17, issue.3, pp.348-375, 1978. ,
DOI : 10.1016/0022-0000(78)90014-4
Computational lambda-calculus and monads, [1989] Proceedings. Fourth Annual Symposium on Logic in Computer Science, pp.14-23, 1989. ,
DOI : 10.1109/LICS.1989.39155
Ynot: Reasoning with the awkward squad, ACM SIGPLAN International Conference on Functional Programming, 2008. ,
Dependently typed programming in agda, Proceedings of TLDI'09, pp.1-2, 2009. ,
Handlers of algebraic effects Held as Part of the Joint European Conferences on Theory and Practice of Software, Programming Languages and Systems, 18th European Symposium on Programming Proceedings, pp.80-94, 2009. ,
Separation logic: A logic for shared mutable data structures, 17th IEEE Symposium on Logic in Computer Science, pp.22-25, 2002. ,
Lwt, Proceedings of the 2008 ACM SIGPLAN workshop on ML, ML '08, pp.3-12, 2008. ,
DOI : 10.1145/1411304.1411307
URL : https://hal.archives-ouvertes.fr/hal-00495983
The essence of functional programming, Proceedings of the 19th ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '92, pp.1-14, 1992. ,
DOI : 10.1145/143165.143169