@incollection(polycontracts:2011, author = "Jo\~ao Belo and Michael Greenberg and Atsushi Igarashi and Benjamin Pierce", year = "2011", title = "Polymorphic Contracts", booktitle = "Programming Languages and Systems", series = "LNCS", volume = "6602", publisher = "Springer", pages = "18--37", doi = "10.1007/978-3-642-19718-5\_2", ) @inproceedings(Bhargavan:2010:MVS, author = "Karthikeyan Bhargavan and C\'{e}dric Fournet and Andrew D. Gordon", year = "2010", title = "Modular verification of security protocol code by typing", booktitle = "POPL'10", publisher = "ACM", pages = "445--456", doi = "10.1145/1706299.1706350", url = "10.1145/1706299.1706350", ) @inproceedings(bocchi.honda:theory-of-design-by-contract, author = "Laura Bocchi and Kohei Honda and Emilio Tuosto and Nobuko Yoshida", year = "2010", title = "A theory of design-by-contract for distributed multiparty interactions", booktitle = "Proceedings of the 21st international conference on Concurrency theory", series = "CONCUR'10", publisher = "Springer", pages = "162--176", doi = "10.1007/978-3-642-15375-4\_12", ) @article(bonelli.compagnoni.gunter:correspondence-assertions-process-synchronization, author = "Eduardo Bonelli and Adriana Compagnoni and Elsa Gunter", year = "2005", title = "Correspondence Assertions for Process Synchronization in Concurrent Communications", journal = "Journal of Functional Programming", volume = "15", pages = "219--247", doi = "10.1017/S095679680400543X", ) @inproceedings(Flanagan:2006:HTC, author = "Cormac Flanagan", year = "2006", title = "Hybrid type checking", booktitle = "Conference record of the 33rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages", series = "POPL'06", publisher = "ACM", pages = "245--256", doi = "10.1145/1111037.1111059", ) @inproceedings(Freeman:1991:ML, author = "Tim Freeman and Frank Pfenning", year = "1991", title = "Refinement types for {ML}", booktitle = "PLDI'91", publisher = "ACM", pages = "268--277", doi = "10.1145/113446.113468", ) @article(Girard87, author = "Jean-Yves Girard", year = "1987", title = "Linear logic", journal = "Theoretical Computer Science", volume = "50", pages = "1--102", doi = "10.1016/0304-3975(87)90045-4", ) @techreport(gordon.fournet:principles-refinement-types, author = "Andrew Gordon and C\'edric Fournet", year = "2009", title = "Principles and applications of refinement types", type = "TR", number = "147", institution = "MSR", doi = "10.3233/978-1-60750-100-8-73", ) @inproceedings(honda.vasconcelos.ea:language-primitives, author = "Kohei Honda and Vasco T. Vasconcelos and Makoto Kubo", year = "1998", title = "Language primitives and type discipline for structured communication-based programming", booktitle = "{ESOP}'98", series = "LNCS", publisher = "Springer", pages = "122--138", doi = "10.1007/BFb0053567", ) @inproceedings(Honda:2008:MAS, author = "Kohei Honda and Nobuko Yoshida and Marco Carbone", year = "2008", title = "Multiparty asynchronous session types", booktitle = "POPL'08", publisher = "ACM", pages = "273--284", doi = "10.1145/1328438.1328472", url = "10.1145/1328438.1328472", ) @inproceedings(mandelbaum:effref, author = "Yitzhak Mandelbaum and David Walker and Robert Harper", year = "2003", title = "An Effective Theory of Type Refinements", booktitle = "ICFP'03", publisher = "ACM", pages = "213--226", doi = "10.1145/944705.944725", ) @inproceedings(mostrous.yoshida:two-session-systems-higher-order, author = "Dimitris Mostrous and Nobuko Yoshida", year = "2007", title = "Two session typing systems for higher-order mobile processes", booktitle = "TLCA'07", series = "LNCS", volume = "4583", publisher = "Springer", pages = "321--335", doi = "10.1007/978-3-540-73228-0\_23", ) @inproceedings(mostrous_yoshida_tlca09, author = "Dimitris Mostrous and Nobuko Yoshida", year = "2009", title = "Session-Based Communication Optimisation for Higher-Order Mobile Processes", booktitle = "TLCA'09", series = "LNCS", volume = "5608", publisher = "Springer", pages = "203--218", doi = "10.1007/978-3-642-02273-9\_16", ) @incollection(Z3:2008, author = "Leonardo de Moura and Nikolaj Bj\/orner", year = "2008", title = "Z3: An Efficient SMT Solver", booktitle = "TACAS", series = "LNCS", volume = "4963", publisher = "Springer", pages = "337--340", doi = "10.1007/978-3-540-78800-3\_24", ) @misc(Fsharp, author = "Microsoft Research", title = "F7: {R}efinement {T}ypes for {F}\#", note = "\url {http://research.microsoft.com/en-us/projects/F7/}", ) @inproceedings(Rondon:2008:LT, author = "Patrick M. Rondon and Ming Kawaguci and Ranjit Jhala", year = "2008", title = "Liquid types", booktitle = "PLDI'08", publisher = "ACM", pages = "159--169", doi = "10.1145/1375581.1375602", ) @inproceedings(toninho.caires.pfenning:dependent-session-types, author = "Bernardo Toninho and Lu\'{\i }s Caires and Frank Pfenning", year = "2011", title = "Dependent session types via intuitionistic linear type theory", booktitle = "Proceedings of the 13th international ACM SIGPLAN symposium on Principles and practices of declarative programming", series = "PPDP'11", publisher = "ACM", pages = "161--172", doi = "10.1145/2003476.2003499", ) @article(vasconcelos:fundamental-sessions, author = "Vasco T. Vasconcelos", year = "2012", title = "Fundamentals of Session Types", journal = "Information and Computation", volume = "217", pages = "52--70", doi = "10.1007/978-3-642-01918-0\_4", url = "http://www.di.fc.ul.pt/~vv/papers/vasconcelos_fundamental-sessions.pdf", note = "Earlier version in SFM'09, volume 5569 of LNCS, pages 158-186. Springer, 2009", doi = "10.1007/978-3-642-01918-0\_4", ) @inproceedings(wadler.findler:well-typed-programs-not-blamed, author = "Philip Wadler and Robert Bruce Findler", year = "2009", title = "Well-typed programs can't be blamed", booktitle = "ESOP'09", publisher = "Springer", pages = "1--16", doi = "10.1007/978-3-642-00590-9\_1", ) @inproceedings(Yoshida:2004:CDT, author = "Nobuko Yoshida", year = "2004", title = "Channel dependent types for higher-order mobile processes", booktitle = "POPL'04", publisher = "ACM", pages = "147--160", doi = "10.1145/964001.964014", )