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