Introduction to set constraint-based program analysis, Science of Computer Programming, vol.35, issue.2-3, pp.79-111, 1999. ,
DOI : 10.1016/S0167-6423(99)00007-6
URL : https://doi.org/10.1016/s0167-6423(99)00007-6
Type inclusion constraints and type inference, Proceedings of the conference on Functional programming languages and computer architecture , FPCA '93, pp.31-41, 1993. ,
DOI : 10.1145/165180.165188
URL : http://www.cs.berkeley.edu/~aiken/publications/papers/fpca93.ps
The ?-Calculus. Studies in logic and the foundations of mathematics, 1984. ,
The ?-Calculus with Types Association for Symbolic Logic, 2013. ,
A Filter Lambda Model and the Completeness of Type Assignment, Journal of Symbolic Logic, vol.48, issue.4, pp.931-940, 1983. ,
Provable isomorphisms of types, Mathematical Structures in Computer Science, vol.19, issue.02, pp.231-247, 1992. ,
DOI : 10.1305/ndjfl/1093883461
Intersection and union types: syntax and semantics, BM94. Franco Barbanera and Simone Martini. Proof-functional connectives and realizability. Archive for Mathematical Logic, pp.202-230189, 1994. ,
Subtyping with union types, intersection types and recursive types, TACS, pp.687-706, 1994. ,
The " relevance " of intersection and union types, Notre Dame Journal of Formal Logic, vol.38, issue.2, pp.246-269, 1997. ,
A Realizability Interpretation for Intersection and Union Types, APLAS, pp.187-205, 2016. ,
DOI : 10.1007/3-540-45927-8_9
URL : https://hal.archives-ouvertes.fr/hal-01317213
Logic and computation in a lambda calculus with intersection and union types, LPAR, pp.173-191, 2010. ,
Tridirectional typechecking, POPL, pp.281-292, 2004. ,
DOI : 10.1145/964001.964025
URL : http://www.cs.cmu.edu/~fp/papers/popl04.pdf
Elaborating intersection and union types, Journal of Functional Programming, vol.12, issue.2-3, pp.133-165, 2014. ,
DOI : 10.1007/BF01211394
Semantic subtyping, Journal of the ACM, vol.55, issue.4, pp.1-1964, 2008. ,
DOI : 10.1145/1391289.1391293
URL : https://hal.archives-ouvertes.fr/hal-00152690
A framework for defining logics, Journal of the ACM, vol.40, issue.1, pp.143-184, 1993. ,
DOI : 10.1145/138027.138060
URL : http://www.cs.cmu.edu/~rwh/papers/lf/jacm93.ps
The simple semantics for Coppo-Dezani-Sall?? types, International Symposium on Programming, pp.212-226, 1982. ,
DOI : 10.1007/3-540-11494-7_15
The Formulae-as-Types Notion of Construction, To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, pp.479-490, 1980. ,
Proof functional connectives, Methods in Mathematical Logic, pp.208-221, 1985. ,
Intersection typed systemàsystem`systemà la Church, Information and Computation, vol.9, issue.205, pp.1371-1386, 2007. ,
DOI : 10.1016/j.entcs.2005.06.015
URL : https://hal.archives-ouvertes.fr/hal-01149611
A Decidable Subtyping Logic for Intersection and Union Types, Research report, vol.19, issue.3, 2017. ,
DOI : 10.1016/S0019-9958(86)80019-5
URL : https://hal.archives-ouvertes.fr/hal-01760641
The completeness of provable realizability., Notre Dame Journal of Formal Logic, vol.30, issue.3, pp.420-441, 1989. ,
DOI : 10.1305/ndjfl/1093635158
An ideal model for recursive polymorphic types, Information and Control, vol.71, issue.1-2, pp.95-130, 1986. ,
DOI : 10.1016/S0019-9958(86)80019-5
Algebraic analysis of entailment I. Logique et Analyse Pfe93. Frank Pfenning. Refinement types for logical frameworks, TYPES, pp.407-428, 1972. ,
Programming with intersection types, union types, and bounded polymorphism, 1991. ,
A type assignment for the strongly normalizable ?-terms Natural deduction: a proof-theoretical study, To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism Pra65. Dag Prawitz, pp.561-577, 1965. ,
Design of the programming language Forsythe, 1996. ,
Deciding equivalence of finite tree automata, Journal of Symbolic Logic, vol.19, issue.3, pp.424-437, 1990. ,