@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}
}
@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}
}
@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}
}
@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}
}
@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}
}
@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}
}
@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}
}
@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}
}
@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}
}
@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}
}
@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}
}
@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}
}
@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}
}
@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}
}
@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}
}
The metadata provided by Dagstuhl Publishing on its webpages, as well as their export formats (such as XML or BibTeX) available at our website, is released under the CC0 1.0 Public Domain Dedication license. That is, you are free to copy, distribute, use, modify, transform, build upon, and produce derived works from our data, even for commercial purposes, all without asking permission. Of course, we are always happy if you provide a link to us as the source of the data.
Read the full CC0 1.0 legal code for the exact terms that apply: https://creativecommons.org/publicdomain/zero/1.0/legalcode
Feedback for Dagstuhl Publishing