Ralph Matthes and Aleksy Schubert. LIPIcs, Volume 26, TYPES'13, Complete Volume. In 19th International Conference on Types for Proofs and Programs (TYPES 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 26, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2014)
@Proceedings{matthes_et_al:LIPIcs.TYPES.2013, title = {{LIPIcs, Volume 26, TYPES'13, Complete Volume}}, booktitle = {19th International Conference on Types for Proofs and Programs (TYPES 2013)}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-72-9}, ISSN = {1868-8969}, year = {2014}, volume = {26}, editor = {Matthes, Ralph and Schubert, Aleksy}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2013}, URN = {urn:nbn:de:0030-drops-46370}, doi = {10.4230/LIPIcs.TYPES.2013}, annote = {Keywords: Applicative (Functional) Programming, Software/Program Verification, Specifying and Verifying and Reasoning about Programs, Mathematical Logic} }
Ralph Matthes and Aleksy Schubert. Frontmatter, Table of Contents, Preface, Conference Organization. In 19th International Conference on Types for Proofs and Programs (TYPES 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 26, pp. i-x, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2014)
@InProceedings{matthes_et_al:LIPIcs.TYPES.2013.i, author = {Matthes, Ralph and Schubert, Aleksy}, title = {{Frontmatter, Table of Contents, Preface, Conference Organization}}, booktitle = {19th International Conference on Types for Proofs and Programs (TYPES 2013)}, pages = {i--x}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-72-9}, ISSN = {1868-8969}, year = {2014}, volume = {26}, editor = {Matthes, Ralph and Schubert, Aleksy}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2013.i}, URN = {urn:nbn:de:0030-drops-46225}, doi = {10.4230/LIPIcs.TYPES.2013.i}, annote = {Keywords: Frontmatter, Table of Contents, Preface, Conference Organization} }
Danel Ahman and Tarmo Uustalu. Update Monads: Cointerpreting Directed Containers. In 19th International Conference on Types for Proofs and Programs (TYPES 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 26, pp. 1-23, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2014)
@InProceedings{ahman_et_al:LIPIcs.TYPES.2013.1, author = {Ahman, Danel and Uustalu, Tarmo}, title = {{Update Monads: Cointerpreting Directed Containers}}, booktitle = {19th International Conference on Types for Proofs and Programs (TYPES 2013)}, pages = {1--23}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-72-9}, ISSN = {1868-8969}, year = {2014}, volume = {26}, editor = {Matthes, Ralph and Schubert, Aleksy}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2013.1}, URN = {urn:nbn:de:0030-drops-46235}, doi = {10.4230/LIPIcs.TYPES.2013.1}, annote = {Keywords: monads and distributive laws, reader, writer and state monads, monoids and monoid actions, directed containers} }
Federico Aschieri and Margherita Zorzi. A "Game Semantical" Intuitionistic Realizability Validating Markov's Principle. In 19th International Conference on Types for Proofs and Programs (TYPES 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 26, pp. 24-44, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2014)
@InProceedings{aschieri_et_al:LIPIcs.TYPES.2013.24, author = {Aschieri, Federico and Zorzi, Margherita}, title = {{A "Game Semantical" Intuitionistic Realizability Validating Markov's Principle}}, booktitle = {19th International Conference on Types for Proofs and Programs (TYPES 2013)}, pages = {24--44}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-72-9}, ISSN = {1868-8969}, year = {2014}, volume = {26}, editor = {Matthes, Ralph and Schubert, Aleksy}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2013.24}, URN = {urn:nbn:de:0030-drops-46245}, doi = {10.4230/LIPIcs.TYPES.2013.24}, annote = {Keywords: Markov's Principle, Intuitionistic Realizability, Heyting Arithmetic, Game Semantics} }
Gilles Barthe, Gustavo Betarte, Juan Diego Campo, Jesús Mauricio Chimento, and Carlos Luna. Formally Verified Implementation of an Idealized Model of Virtualization. In 19th International Conference on Types for Proofs and Programs (TYPES 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 26, pp. 45-63, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2014)
@InProceedings{barthe_et_al:LIPIcs.TYPES.2013.45, author = {Barthe, Gilles and Betarte, Gustavo and Campo, Juan Diego and Chimento, Jes\'{u}s Mauricio and Luna, Carlos}, title = {{Formally Verified Implementation of an Idealized Model of Virtualization}}, booktitle = {19th International Conference on Types for Proofs and Programs (TYPES 2013)}, pages = {45--63}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-72-9}, ISSN = {1868-8969}, year = {2014}, volume = {26}, editor = {Matthes, Ralph and Schubert, Aleksy}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2013.45}, URN = {urn:nbn:de:0030-drops-46254}, doi = {10.4230/LIPIcs.TYPES.2013.45}, annote = {Keywords: virtualization, Cache and TLB, Executable specification, Error management, Isolation} }
Stefano Berardi and Silvia Steila. Ramsey Theorem for Pairs As a Classical Principle in Intuitionistic Arithmetic. In 19th International Conference on Types for Proofs and Programs (TYPES 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 26, pp. 64-83, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2014)
@InProceedings{berardi_et_al:LIPIcs.TYPES.2013.64, author = {Berardi, Stefano and Steila, Silvia}, title = {{Ramsey Theorem for Pairs As a Classical Principle in Intuitionistic Arithmetic}}, booktitle = {19th International Conference on Types for Proofs and Programs (TYPES 2013)}, pages = {64--83}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-72-9}, ISSN = {1868-8969}, year = {2014}, volume = {26}, editor = {Matthes, Ralph and Schubert, Aleksy}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2013.64}, URN = {urn:nbn:de:0030-drops-46269}, doi = {10.4230/LIPIcs.TYPES.2013.64}, annote = {Keywords: Formalization, Constructivism, Classical logic, Ramsey Theorem} }
Ulrich Berger, Monika Seisenberger, and Gregory J. M. Woods. Extracting Imperative Programs from Proofs: In-place Quicksort. In 19th International Conference on Types for Proofs and Programs (TYPES 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 26, pp. 84-106, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2014)
@InProceedings{berger_et_al:LIPIcs.TYPES.2013.84, author = {Berger, Ulrich and Seisenberger, Monika and Woods, Gregory J. M.}, title = {{Extracting Imperative Programs from Proofs: In-place Quicksort}}, booktitle = {19th International Conference on Types for Proofs and Programs (TYPES 2013)}, pages = {84--106}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-72-9}, ISSN = {1868-8969}, year = {2014}, volume = {26}, editor = {Matthes, Ralph and Schubert, Aleksy}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2013.84}, URN = {urn:nbn:de:0030-drops-46274}, doi = {10.4230/LIPIcs.TYPES.2013.84}, annote = {Keywords: Program Extraction, Verification, Realizability, Imperative Programs, In-Place Quicksort,Computational Monads, Minlog} }
Marc Bezem, Thierry Coquand, and Simon Huber. A Model of Type Theory in Cubical Sets. In 19th International Conference on Types for Proofs and Programs (TYPES 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 26, pp. 107-128, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2014)
@InProceedings{bezem_et_al:LIPIcs.TYPES.2013.107, author = {Bezem, Marc and Coquand, Thierry and Huber, Simon}, title = {{A Model of Type Theory in Cubical Sets}}, booktitle = {19th International Conference on Types for Proofs and Programs (TYPES 2013)}, pages = {107--128}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-72-9}, ISSN = {1868-8969}, year = {2014}, volume = {26}, editor = {Matthes, Ralph and Schubert, Aleksy}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2013.107}, URN = {urn:nbn:de:0030-drops-46284}, doi = {10.4230/LIPIcs.TYPES.2013.107}, annote = {Keywords: Models of dependent type theory, cubical sets, Univalent Foundations} }
Mario Coppo, Mariangiola Dezani-Ciancaglini, Ines Margaria, and Maddalena Zacchi. Isomorphism of "Functional" Intersection Types. In 19th International Conference on Types for Proofs and Programs (TYPES 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 26, pp. 129-149, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2014)
@InProceedings{coppo_et_al:LIPIcs.TYPES.2013.129, author = {Coppo, Mario and Dezani-Ciancaglini, Mariangiola and Margaria, Ines and Zacchi, Maddalena}, title = {{Isomorphism of "Functional" Intersection Types}}, booktitle = {19th International Conference on Types for Proofs and Programs (TYPES 2013)}, pages = {129--149}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-72-9}, ISSN = {1868-8969}, year = {2014}, volume = {26}, editor = {Matthes, Ralph and Schubert, Aleksy}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2013.129}, URN = {urn:nbn:de:0030-drops-46296}, doi = {10.4230/LIPIcs.TYPES.2013.129}, annote = {Keywords: Type Isomorphism, Lambda calculus, Intersection Types} }
Joëlle Despeyroux and Kaustuv Chaudhuri. A Hybrid Linear Logic for Constrained Transition Systems. In 19th International Conference on Types for Proofs and Programs (TYPES 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 26, pp. 150-168, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2014)
@InProceedings{despeyroux_et_al:LIPIcs.TYPES.2013.150, author = {Despeyroux, Jo\"{e}lle and Chaudhuri, Kaustuv}, title = {{A Hybrid Linear Logic for Constrained Transition Systems}}, booktitle = {19th International Conference on Types for Proofs and Programs (TYPES 2013)}, pages = {150--168}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-72-9}, ISSN = {1868-8969}, year = {2014}, volume = {26}, editor = {Matthes, Ralph and Schubert, Aleksy}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2013.150}, URN = {urn:nbn:de:0030-drops-46302}, doi = {10.4230/LIPIcs.TYPES.2013.150}, annote = {Keywords: Linear logic, hybrid logic, stochastic pi-calculus, focusing, adequacy} }
Hugo Herbelin and Arnaud Spiwack. The Rooster and the Syntactic Bracket. In 19th International Conference on Types for Proofs and Programs (TYPES 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 26, pp. 169-187, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2014)
@InProceedings{herbelin_et_al:LIPIcs.TYPES.2013.169, author = {Herbelin, Hugo and Spiwack, Arnaud}, title = {{The Rooster and the Syntactic Bracket}}, booktitle = {19th International Conference on Types for Proofs and Programs (TYPES 2013)}, pages = {169--187}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-72-9}, ISSN = {1868-8969}, year = {2014}, volume = {26}, editor = {Matthes, Ralph and Schubert, Aleksy}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2013.169}, URN = {urn:nbn:de:0030-drops-46318}, doi = {10.4230/LIPIcs.TYPES.2013.169}, annote = {Keywords: Coq, Calculus of inductive constructions, Impredicativity, Strictly positive type families, Inductive type families} }
Danko Ilik and Keiko Nakata. A Direct Version of Veldman's Proof of Open Induction on Cantor Space via Delimited Control Operators. In 19th International Conference on Types for Proofs and Programs (TYPES 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 26, pp. 188-201, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2014)
@InProceedings{ilik_et_al:LIPIcs.TYPES.2013.188, author = {Ilik, Danko and Nakata, Keiko}, title = {{A Direct Version of Veldman's Proof of Open Induction on Cantor Space via Delimited Control Operators}}, booktitle = {19th International Conference on Types for Proofs and Programs (TYPES 2013)}, pages = {188--201}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-72-9}, ISSN = {1868-8969}, year = {2014}, volume = {26}, editor = {Matthes, Ralph and Schubert, Aleksy}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2013.188}, URN = {urn:nbn:de:0030-drops-46320}, doi = {10.4230/LIPIcs.TYPES.2013.188}, annote = {Keywords: Open Induction, Axiom of Choice, Double Negation Shift, Markov's Principle, delimited control operators} }
Christian Retoré. The Montagovian Generative Lexicon Lambda Ty_n: a Type Theoretical Framework for Natural Language Semantics. In 19th International Conference on Types for Proofs and Programs (TYPES 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 26, pp. 202-229, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2014)
@InProceedings{retore:LIPIcs.TYPES.2013.202, author = {Retor\'{e}, Christian}, title = {{The Montagovian Generative Lexicon Lambda Ty\underlinen: a Type Theoretical Framework for Natural Language Semantics}}, booktitle = {19th International Conference on Types for Proofs and Programs (TYPES 2013)}, pages = {202--229}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-72-9}, ISSN = {1868-8969}, year = {2014}, volume = {26}, editor = {Matthes, Ralph and Schubert, Aleksy}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2013.202}, URN = {urn:nbn:de:0030-drops-46336}, doi = {10.4230/LIPIcs.TYPES.2013.202}, annote = {Keywords: type theory, computational linguistics} }
Leonardo Rodríguez, Daniel Fridlender, and Miguel Pagano. A Certified Extension of the Krivine Machine for a Call-by-Name Higher-Order Imperative Language. In 19th International Conference on Types for Proofs and Programs (TYPES 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 26, pp. 230-250, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2014)
@InProceedings{rodriguez_et_al:LIPIcs.TYPES.2013.230, author = {Rodr{\'\i}guez, Leonardo and Fridlender, Daniel and Pagano, Miguel}, title = {{A Certified Extension of the Krivine Machine for a Call-by-Name Higher-Order Imperative Language}}, booktitle = {19th International Conference on Types for Proofs and Programs (TYPES 2013)}, pages = {230--250}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-72-9}, ISSN = {1868-8969}, year = {2014}, volume = {26}, editor = {Matthes, Ralph and Schubert, Aleksy}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2013.230}, URN = {urn:nbn:de:0030-drops-46343}, doi = {10.4230/LIPIcs.TYPES.2013.230}, annote = {Keywords: Abstract Machines, Compiler Correctness, Big-step semantics} }
Tao Xue. Definitional Extension in Type Theory. In 19th International Conference on Types for Proofs and Programs (TYPES 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 26, pp. 251-269, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2014)
@InProceedings{xue:LIPIcs.TYPES.2013.251, author = {Xue, Tao}, title = {{Definitional Extension in Type Theory}}, booktitle = {19th International Conference on Types for Proofs and Programs (TYPES 2013)}, pages = {251--269}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-72-9}, ISSN = {1868-8969}, year = {2014}, volume = {26}, editor = {Matthes, Ralph and Schubert, Aleksy}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2013.251}, URN = {urn:nbn:de:0030-drops-46352}, doi = {10.4230/LIPIcs.TYPES.2013.251}, annote = {Keywords: conservative extension, definitional extension, subtype, coercive subtyping} }
Feedback for Dagstuhl Publishing