MiniAgda: Integrating Sized and Dependent Types, Workshop on Partiality And Recursion in Interactive Theorem Provers (PAR), 2010. ,
DOI : 10.4204/EPTCS.43.2
????: Dependent Types without the Sugar, Functional and Logic Programming, pp.40-55, 2010. ,
DOI : 10.1007/978-3-642-12251-4_5
Subtyping recursive types, ACM Transactions on Programming Languages and Systems, vol.15, issue.4, pp.575-631, 1993. ,
A very modal model of a modern, major, general type system, ACM Symposium on Principles of Programming Languages (POPL), pp.109-122, 2007. ,
URL : https://hal.archives-ouvertes.fr/hal-00150978
Parameterised notions of computation, Journal of Functional Programming, vol.22, issue.3-4, pp.3-4355, 2009. ,
DOI : 10.1145/158511.158524
The Lambda Calculus, Its Syntax and Semantics, 1984. ,
A metric model of lambda calculus with guarded recursion, 2010. ,
The categorytheoretic solution of recursive metric-space quations, 2009. ,
Realizability Semantics of Parametric Polymorphism, General References, and Recursive Types, Mathematical Structures in Computer Science, vol.11, issue.4, 2010. ,
DOI : 10.1137/0211062
Coinductive axiomatization of recursive type equality and subtyping, Fundamenta Informaticae, vol.33, pp.309-338, 1998. ,
DOI : 10.1007/3-540-62688-3_29
Functional translation of a calculus of capabilities, ACM International Conference on Functional Programming (ICFP), pp.213-224, 2008. ,
A simplified account of polymorphic references, Information Processing Letters, vol.51, issue.4, pp.201-206, 1994. ,
DOI : 10.1016/0020-0190(94)90120-1
A theory of indirection via approximation, ACM Symposium on Principles of Programming Languages (POPL), 2010. ,
Bisimulation in untyped lambda calculus: Böhm trees and bisimulation up to context, Mathematical Foundations of Programming Semantics, pp.346-374, 1999. ,
Possible world semantics for general storage in callby-value, Computer Science Logic, 2002. ,
Polymorphic type inference and containment. Information and Computation, pp.211-249, 1988. ,
Notions of computation and monads. Information and Computation, 1991. ,
An abstract monadic semantics for value recursion, Informatique théorique et applications, pp.377-400, 2004. ,
DOI : 10.1051/ita:2004018
Full abstraction in a metalanguage for state, Workshop on Syntax and Semantics of Low Level Languages, 2010. ,
A modality for recursion, Proceedings Fifteenth Annual IEEE Symposium on Logic in Computer Science (Cat. No.99CB36332), pp.255-266, 2000. ,
DOI : 10.1109/LICS.2000.855774
Fixed-Point Logic with the Approximation Modality and Its Kripke Completeness, International Symposium on Theoretical Aspects of Computer Software (TACS), pp.165-182, 2001. ,
DOI : 10.1007/3-540-45500-0_8
Hoare type theory, polymorphism and separation, Journal of Functional Programming, vol.18, pp.5-6, 2008. ,
From Algol to polymorphic linear lambda-calculus, Journal of the ACM, vol.47, issue.1, pp.167-223, 2000. ,
Imperative functional programming, Proceedings of the 20th ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '93, pp.71-84, 1993. ,
DOI : 10.1145/158511.158524
Hiding Local State in Direct Style: A Higher-Order Anti-Frame Rule, 2008 23rd Annual IEEE Symposium on Logic in Computer Science, pp.331-340, 2008. ,
DOI : 10.1109/LICS.2008.16
A formalization of Nakano's type system. http: //gallium.inria.fr, 2009. ,
The electronic FORK, 2010. ,
A typed store-passing translation for general references (extended version), 2010. ,
Nested Hoare Triples and Frame Rules for Higher-Order Store, Computer Science Logic, pp.440-454, 2009. ,
DOI : 10.1142/6284
A Semantic Foundation for Hidden State, International Conference on Foundations of Software Science and Computation Structures (FOSSACS), pp.2-17, 2010. ,
DOI : 10.1007/978-3-642-12032-9_2
Fundamental concepts in programming languages . Higher-Order and Symbolic Computation, pp.11-49, 2000. ,
Parallel reductions in ?-calculus. Information and Computation, pp.120-127, 1995. ,
Abstract models of storage. Higher-Order and Symbolic Computation, pp.119-129, 2000. ,
A syntactic approach to type soundness, Information and Computation, vol.115, issue.1, pp.38-94, 1994. ,