@article(ill1, author = "Antonio Bucciarelli and Thomas Ehrhard", year = "2000", title = "On Phase Semantics and Denotational Semantics in Multiplicative-Additive Linear Logic", journal = "Ann. Pure Appl. Logic", volume = "102", number = "3", pages = "247--282", doi = "10.1016/S0168-0072(99)00040-8", url = "http://www.pps.univ-paris-diderot.fr/~buccia/PUBLI/apal00.ps", ) @article(ill2, author = "Antonio Bucciarelli and Thomas Ehrhard", year = "2001", title = "On phase semantics and denotational semantics: the exponentials", journal = "Ann. Pure Appl. Logic", volume = "109", number = "3", pages = "205--241", doi = "10.1016/S0168-0072(00)00056-7", url = "http://www.pps.univ-paris-diderot.fr/~buccia/PUBLI/apal01.ps", ) @article(carvalho, author = "Daniel de Carvalho", year = "2009", title = "Execution Time of lambda-Terms via Denotational Semantics and Intersection Types", journal = "CoRR", volume = "abs/0905.4251", url = "http://arxiv.org/abs/0905.4251", ) @inproceedings(ehrhard-collapse-2, author = "Thomas Ehrhard", year = "2012", title = "Collapsing non-idempotent intersection types", editor = "Patrick C{\'e}gielski and Arnaud Durand", booktitle = "CSL", series = "LIPIcs", volume = "16", publisher = "Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik", pages = "259--273", url = "http://dx.doi.org/10.4230/LIPIcs.CSL.2012.259", ) @article(ehrhard-collapse, author = "Thomas Ehrhard", year = "2012", title = "The Scott model of linear logic is the extensional collapse of its relational model", journal = "Theor. Comput. Sci.", volume = "424", pages = "20--45", doi = "10.1016/j.tcs.2011.11.027", url = "http://www.pps.univ-paris-diderot.fr/~ehrhard/pub/relscott.pdf", ) @misc(tensorial-logic-with-colours, author = "Charles Grellois and Paul{-}Andr{\'{e}} Melli{\`{e}}s", year = "2015", title = "Tensorial logic with colours and higher-order model checking", howpublished = "submitted, \url {http://arxiv.org/abs/1501.04789}", ) @inproceedings(cpda, author = "Matthew Hague and Andrzej S. Murawski and C.-H. Luke Ong and Olivier Serre", year = "2008", title = "Collapsible Pushdown Automata and Recursion Schemes", booktitle = "LICS", publisher = "IEEE Computer Society", pages = "452--461", doi = "10.1109/LICS.2008.34", url = "http://www.cs.ox.ac.uk/people/luke.ong/personal/publications/cpda-long.pdf", ) @inproceedings(koba09, author = "Naoki Kobayashi", year = "2009", title = "Types and higher-order recursion schemes for verification of higher-order programs", editor = "Zhong Shao and Benjamin C. Pierce", booktitle = "POPL", publisher = "ACM", pages = "416--428", doi = "10.1145/1480881.1480933", url = "http://www.kb.is.s.u-tokyo.ac.jp/~koba/papers/popl2009.pdf", ) @inproceedings(kobayashi-ong, author = "Naoki Kobayashi and C.-H. Luke Ong", year = "2009", title = "A Type System Equivalent to the Modal Mu-Calculus Model Checking of Higher-Order Recursion Schemes", booktitle = "LICS", publisher = "IEEE Computer Society", pages = "179--188", doi = "10.1109/LICS.2009.29", url = "http://www.cs.ox.ac.uk/people/luke.ong/personal/publications/lics09-ko-long.pdf", ) @inproceedings(ong, author = "C.-H. Luke Ong", year = "2006", title = "On Model-Checking Trees Generated by Higher-Order Recursion Schemes", booktitle = "LICS", publisher = "IEEE Computer Society", pages = "81--90", doi = "10.1109/LICS.2006.38", url = "http://www.cs.ox.ac.uk/people/luke.ong/personal/publications/ntrees.pdf", ) @inproceedings(ong-tsukada, author = "C.-H. Luke Ong and Takeshi Tsukada", year = "2012", title = "Two-Level Game Semantics, Intersection Types, and Recursion Schemes", editor = "Artur Czumaj and Kurt Mehlhorn and Andrew M. Pitts and Roger Wattenhofer", booktitle = "ICALP (2)", series = "Lecture Notes in Computer Science", volume = "7392", publisher = "Springer", pages = "325--336", doi = "10.1007/978-3-642-31585-5\_31", url = "http://www.cs.ox.ac.uk/people/luke.ong/personal/publications/icalp12.pdf", ) @inproceedings(salvati-walukiewicz-krivine, author = "Sylvain Salvati and Igor Walukiewicz", year = "2012", title = "Recursive Schemes, Krivine Machines, and Collapsible Pushdown Automata", editor = "Alain Finkel and J{\'e}r{\^o}me Leroux and Igor Potapov", booktitle = "RP", series = "Lecture Notes in Computer Science", volume = "7550", publisher = "Springer", pages = "6--20", doi = "10.1007/978-3-642-33512-9\_2", ) @inproceedings(salvati2, author = "Sylvain Salvati and Igor Walukiewicz", year = "2013", title = "Evaluation is MSOL-compatible", editor = "Anil Seth and Nisheeth K. Vishnoi", booktitle = "FSTTCS", series = "LIPIcs", volume = "24", publisher = "Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik", pages = "103--114", doi = "10.4230/LIPIcs.FSTTCS.2013.103", url = "http://hal.inria.fr/docs/00/77/31/26/PDF/m.pdf", ) @inproceedings(salvati, author = "Sylvain Salvati and Igor Walukiewicz", year = "2013", title = "Using Models to Model-Check Recursive Schemes", editor = "Masahito Hasegawa", booktitle = "TLCA", series = "Lecture Notes in Computer Science", volume = "7941", publisher = "Springer", pages = "189--204", doi = "10.1007/978-3-642-38946-7\_15", url = "http://hal.archives-ouvertes.fr/docs/00/74/12/39/PDF/m.pdf", ) @inproceedings(terui, author = "Kazushige Terui", year = "2012", title = "Semantic Evaluation, Intersection Types and Complexity of Simply Typed Lambda Calculus", editor = "Ashish Tiwari", booktitle = "RTA", series = "LIPIcs", volume = "15", publisher = "Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik", pages = "323--338", doi = "10.4230/LIPIcs.RTA.2012.323", url = "http://www.kurims.kyoto-u.ac.jp/~terui/nbi8.pdf", )