LIPIcs, Volume 26
TYPES 2013, April 22-26, 2013, Toulouse, France
Editors: Ralph Matthes and Aleksy Schubert
Published in: LIPIcs, Volume 97, 22nd International Conference on Types for Proofs and Programs (TYPES 2016)
Jacek Chrzaszcz, Aleksy Schubert, and Jakub Zakrzewski. Coq Support in HAHA. In 22nd International Conference on Types for Proofs and Programs (TYPES 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 97, pp. 8:1-8:26, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
@InProceedings{chrzaszcz_et_al:LIPIcs.TYPES.2016.8, author = {Chrzaszcz, Jacek and Schubert, Aleksy and Zakrzewski, Jakub}, title = {{Coq Support in HAHA}}, booktitle = {22nd International Conference on Types for Proofs and Programs (TYPES 2016)}, pages = {8:1--8:26}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-065-1}, ISSN = {1868-8969}, year = {2018}, volume = {97}, editor = {Ghilezan, Silvia and Geuvers, Herman and Ivetic, Jelena}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2016.8}, URN = {urn:nbn:de:0030-drops-98562}, doi = {10.4230/LIPIcs.TYPES.2016.8}, annote = {Keywords: Hoare logic, program verification, Coq theorem prover, teaching} }
Published in: LIPIcs, Volume 52, 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)
Marcin Benke, Aleksy Schubert, and Daria Walukiewicz-Chrzaszcz. Synthesis of Functional Programs with Help of First-Order Intuitionistic Logic. In 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 52, pp. 12:1-12:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
@InProceedings{benke_et_al:LIPIcs.FSCD.2016.12, author = {Benke, Marcin and Schubert, Aleksy and Walukiewicz-Chrzaszcz, Daria}, title = {{Synthesis of Functional Programs with Help of First-Order Intuitionistic Logic}}, booktitle = {1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)}, pages = {12:1--12:16}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-010-1}, ISSN = {1868-8969}, year = {2016}, volume = {52}, editor = {Kesner, Delia and Pientka, Brigitte}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2016.12}, URN = {urn:nbn:de:0030-drops-59765}, doi = {10.4230/LIPIcs.FSCD.2016.12}, annote = {Keywords: ML, program synthesis} }
Published in: LIPIcs, Volume 39, 20th International Conference on Types for Proofs and Programs (TYPES 2014)
Aleksy Schubert, Pawel Urzyczyn, and Daria Walukiewicz-Chrzaszcz. Restricted Positive Quantification Is Not Elementary. In 20th International Conference on Types for Proofs and Programs (TYPES 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 39, pp. 251-273, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
@InProceedings{schubert_et_al:LIPIcs.TYPES.2014.251, author = {Schubert, Aleksy and Urzyczyn, Pawel and Walukiewicz-Chrzaszcz, Daria}, title = {{Restricted Positive Quantification Is Not Elementary}}, booktitle = {20th International Conference on Types for Proofs and Programs (TYPES 2014)}, pages = {251--273}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-88-0}, ISSN = {1868-8969}, year = {2015}, volume = {39}, editor = {Herbelin, Hugo and Letouzey, Pierre and Sozeau, Matthieu}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2014.251}, URN = {urn:nbn:de:0030-drops-55002}, doi = {10.4230/LIPIcs.TYPES.2014.251}, annote = {Keywords: constructive logic, complexity, automata theory} }
Published in: LIPIcs, Volume 41, 24th EACSL Annual Conference on Computer Science Logic (CSL 2015)
Aleksy Schubert, Wil Dekkers, and Henk P. Barendregt. Automata Theoretic Account of Proof Search. In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 41, pp. 128-143, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
@InProceedings{schubert_et_al:LIPIcs.CSL.2015.128, author = {Schubert, Aleksy and Dekkers, Wil and Barendregt, Henk P.}, title = {{Automata Theoretic Account of Proof Search}}, booktitle = {24th EACSL Annual Conference on Computer Science Logic (CSL 2015)}, pages = {128--143}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-90-3}, ISSN = {1868-8969}, year = {2015}, volume = {41}, editor = {Kreutzer, Stephan}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2015.128}, URN = {urn:nbn:de:0030-drops-54113}, doi = {10.4230/LIPIcs.CSL.2015.128}, annote = {Keywords: simple types, automata, trees, languages of proofs} }
Published in: LIPIcs, Volume 26, 19th International Conference on Types for Proofs and Programs (TYPES 2013)
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-dev.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} }
Published in: LIPIcs, Volume 26, 19th International Conference on Types for Proofs and Programs (TYPES 2013)
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-dev.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} }
Published in: LIPIcs, Volume 26, 19th International Conference on Types for Proofs and Programs (TYPES 2013)
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-dev.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} }
Published in: LIPIcs, Volume 26, 19th International Conference on Types for Proofs and Programs (TYPES 2013)
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-dev.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} }
Published in: LIPIcs, Volume 26, 19th International Conference on Types for Proofs and Programs (TYPES 2013)
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-dev.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} }
Published in: LIPIcs, Volume 26, 19th International Conference on Types for Proofs and Programs (TYPES 2013)
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-dev.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} }
Published in: LIPIcs, Volume 26, 19th International Conference on Types for Proofs and Programs (TYPES 2013)
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-dev.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} }
Published in: LIPIcs, Volume 26, 19th International Conference on Types for Proofs and Programs (TYPES 2013)
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-dev.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} }
Published in: LIPIcs, Volume 26, 19th International Conference on Types for Proofs and Programs (TYPES 2013)
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-dev.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} }
Published in: LIPIcs, Volume 26, 19th International Conference on Types for Proofs and Programs (TYPES 2013)
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-dev.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} }
Feedback for Dagstuhl Publishing