H. P. Barendregt (1984):
The Lambda Calculus, its Syntax and Semantics, Revised second edition.
North-Holland.
Henk Barendregt, Mario Coppo & Mariangiola Dezani-Ciancaglini (1983):
A filter lambda model and the completeness of type assignment.
The journal of symbolic logic 48(4),
pp. 931–940,
doi:10.2307/2273659.
M. Coppo & M. Dezani-Ciancaglini (1980):
An extension of the basic functionality theory for the λ-calculus..
Notre Dame Journal of Formal Logic 21(4),
pp. 685–693,
doi:10.1305/ndjfl/1093883253.
Luis Damas & Robin Milner (1982):
Principal Type-schemes for Functional Programs.
In: Proceedings of the 9th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages,
POPL '82.
ACM,
pp. 207–212,
doi:10.1145/582153.582176.
Jean-Christophe Filliâtre (2013):
One Logic To Use Them All.
In: 24th International Conference on Automated Deduction (CADE-24),
Lecture Notes in Artificial Intelligence 7898.
Springer,
Lake Placid, USA,
pp. 1–20,
doi:10.1007/978-3-642-38574-2_1.
Jean-Christophe Filliâtre & Andrei Paskevich (2013):
Why3 — Where Programs Meet Provers.
In: Matthias Felleisen & Philippa Gardner: Proceedings of the 22nd European Symposium on Programming,
Lecture Notes in Computer Science 7792.
Springer,
pp. 125–128,
doi:10.1007/978-3-642-37036-6_8.
Cormac Flanagan, Amr Sabry, Bruce F. Duba & Matthias Felleisen (1993):
The Essence of Compiling with Continuations.
In: Proceedings of the ACM SIGPLAN 1993 Conference on Programming Language Design and Implementation,
PLDI '93.
ACM,
pp. 237–247,
doi:10.1145/155090.155113.
Tim Freeman & Frank Pfenning (1991):
Refinement Types for ML.
In: Proceedings of the ACM SIGPLAN 1991 Conference on Programming Language Design and Implementation,
PLDI '91.
ACM,
pp. 268–277,
doi:10.1145/113445.113468.
Trevor Jim (1995):
Rank 2 type systems and recursive definitions.
Massachusetts Institute of Technology, Cambridge, MA.
A. J. Kfoury & J. B. Wells (1999):
Principality and Decidable Type Inference for Finite-rank Intersection Types.
In: Proceedings of the 26th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages,
POPL '99.
ACM,
pp. 161–174,
doi:10.1145/292540.292556.
Kenneth Knowles & Cormac Flanagan (2010):
Hybrid Type Checking.
ACM Trans. Program. Lang. Syst. 32(2),
pp. 6:1–6:34,
doi:10.1145/1667048.1667051.
Charles Gregory Nelson (1980):
Techniques for Program Verification,
Stanford, CA, USA.
AAI8011683.
C.-H. Luke Ong & Takeshi Tsukada (2012):
Two-level Game Semantics, Intersection Types, and Recursion Schemes.
In: Proceedings of the 39th International Colloquium Conference on Automata, Languages, and Programming - Volume Part II,
ICALP'12.
Springer-Verlag,
pp. 325–336,
doi:10.1007/978-3-642-31585-5_31.
Mário Pereira (2014):
Liquid Intersection Types.
Faculdade de Ciências da Universidade do Porto.
http://www.dcc.fc.up.pt/~mariopereira/msc_thesis.pdf.
Patrick M. Rondon, Ming Kawaguci & Ranjit Jhala (2008):
Liquid Types.
In: Proceedings of the 2008 ACM SIGPLAN Conference on Programming Language Design and Implementation,
PLDI '08.
ACM,
pp. 159–169,
doi:10.1145/1375581.1375602.
Robert E. Shostak (1984):
Deciding Combinations of Theories.
J. ACM 31(1),
pp. 1–12,
doi:10.1145/2422.322411.
Niki Vazou, Patrick M. Rondon & Ranjit Jhala (2013):
Abstract Refinement Types.
In: Proceedings of the 22Nd European Conference on Programming Languages and Systems,
ESOP'13.
Springer-Verlag,
pp. 209–228,
doi:10.1007/978-3-642-37036-6_13.
eptcs@eptcs.org