LIPIcs, Volume 26
TYPES 2013, April 22-26, 2013, Toulouse, France
Editors: Ralph Matthes and Aleksy Schubert
Published in: LIPIcs, Volume 269, 28th International Conference on Types for Proofs and Programs (TYPES 2022)
Kobe Wullaert, Ralph Matthes, and Benedikt Ahrens. Univalent Monoidal Categories. In 28th International Conference on Types for Proofs and Programs (TYPES 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 269, pp. 15:1-15:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
@InProceedings{wullaert_et_al:LIPIcs.TYPES.2022.15, author = {Wullaert, Kobe and Matthes, Ralph and Ahrens, Benedikt}, title = {{Univalent Monoidal Categories}}, booktitle = {28th International Conference on Types for Proofs and Programs (TYPES 2022)}, pages = {15:1--15:21}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-285-3}, ISSN = {1868-8969}, year = {2023}, volume = {269}, editor = {Kesner, Delia and P\'{e}drot, Pierre-Marie}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2022.15}, URN = {urn:nbn:de:0030-drops-184580}, doi = {10.4230/LIPIcs.TYPES.2022.15}, annote = {Keywords: Univalence, Monoidal categories, Rezk completion, Displayed (bi)categories, Proof assistant Coq, UniMath library} }
Published in: LIPIcs, Volume 239, 27th International Conference on Types for Proofs and Programs (TYPES 2021)
Yuta Takahashi. Size-Based Termination for Non-Positive Types in Simply Typed Lambda-Calculus. In 27th International Conference on Types for Proofs and Programs (TYPES 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 239, pp. 12:1-12:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
@InProceedings{takahashi:LIPIcs.TYPES.2021.12, author = {Takahashi, Yuta}, title = {{Size-Based Termination for Non-Positive Types in Simply Typed Lambda-Calculus}}, booktitle = {27th International Conference on Types for Proofs and Programs (TYPES 2021)}, pages = {12:1--12:23}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-254-9}, ISSN = {1868-8969}, year = {2022}, volume = {239}, editor = {Basold, Henning and Cockx, Jesper and Ghilezan, Silvia}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2021.12}, URN = {urn:nbn:de:0030-drops-167811}, doi = {10.4230/LIPIcs.TYPES.2021.12}, annote = {Keywords: termination, higher-order rewriting, non-positive types, inductive types} }
Published in: LIPIcs, Volume 188, 26th International Conference on Types for Proofs and Programs (TYPES 2020)
Andreas Abel. On Model-Theoretic Strong Normalization for Truth-Table Natural Deduction. In 26th International Conference on Types for Proofs and Programs (TYPES 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 188, pp. 1:1-1:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
@InProceedings{abel:LIPIcs.TYPES.2020.1, author = {Abel, Andreas}, title = {{On Model-Theoretic Strong Normalization for Truth-Table Natural Deduction}}, booktitle = {26th International Conference on Types for Proofs and Programs (TYPES 2020)}, pages = {1:1--1:21}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-182-5}, ISSN = {1868-8969}, year = {2021}, volume = {188}, editor = {de'Liguoro, Ugo and Berardi, Stefano and Altenkirch, Thorsten}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2020.1}, URN = {urn:nbn:de:0030-drops-138805}, doi = {10.4230/LIPIcs.TYPES.2020.1}, annote = {Keywords: Natural deduction, Permutative conversion, Reducibility, Strong normalization, Truth table} }
Published in: LIPIcs, Volume 188, 26th International Conference on Types for Proofs and Programs (TYPES 2020)
José Espírito Santo, Ralph Matthes, and Luís Pinto. Coinductive Proof Search for Polarized Logic with Applications to Full Intuitionistic Propositional Logic. In 26th International Conference on Types for Proofs and Programs (TYPES 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 188, pp. 4:1-4:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
@InProceedings{espiritosanto_et_al:LIPIcs.TYPES.2020.4, author = {Esp{\'\i}rito Santo, Jos\'{e} and Matthes, Ralph and Pinto, Lu{\'\i}s}, title = {{Coinductive Proof Search for Polarized Logic with Applications to Full Intuitionistic Propositional Logic}}, booktitle = {26th International Conference on Types for Proofs and Programs (TYPES 2020)}, pages = {4:1--4:24}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-182-5}, ISSN = {1868-8969}, year = {2021}, volume = {188}, editor = {de'Liguoro, Ugo and Berardi, Stefano and Altenkirch, Thorsten}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2020.4}, URN = {urn:nbn:de:0030-drops-138837}, doi = {10.4230/LIPIcs.TYPES.2020.4}, annote = {Keywords: Inhabitation problems, Coinduction, Lambda-calculus, Polarized logic} }
Published in: LIPIcs, Volume 130, 24th International Conference on Types for Proofs and Programs (TYPES 2018)
Ulrich Berger, Ralph Matthes, and Anton Setzer. Martin Hofmann’s Case for Non-Strictly Positive Data Types. In 24th International Conference on Types for Proofs and Programs (TYPES 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 130, pp. 1:1-1:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
@InProceedings{berger_et_al:LIPIcs.TYPES.2018.1, author = {Berger, Ulrich and Matthes, Ralph and Setzer, Anton}, title = {{Martin Hofmann’s Case for Non-Strictly Positive Data Types}}, booktitle = {24th International Conference on Types for Proofs and Programs (TYPES 2018)}, pages = {1:1--1:22}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-106-1}, ISSN = {1868-8969}, year = {2019}, volume = {130}, editor = {Dybjer, Peter and Esp{\'\i}rito Santo, Jos\'{e} and Pinto, Lu{\'\i}s}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2018.1}, URN = {urn:nbn:de:0030-drops-114052}, doi = {10.4230/LIPIcs.TYPES.2018.1}, annote = {Keywords: non strictly-positive data types, breadth-first traversal, program verification, Mendler-style recursion, System F, theorem proving, Coq, Agda, Haskell} }
Published in: LIPIcs, Volume 69, 21st International Conference on Types for Proofs and Programs (TYPES 2015) (2018)
Benedikt Ahrens and Ralph Matthes. Heterogeneous Substitution Systems Revisited. In 21st International Conference on Types for Proofs and Programs (TYPES 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 69, pp. 2:1-2:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
@InProceedings{ahrens_et_al:LIPIcs.TYPES.2015.2, author = {Ahrens, Benedikt and Matthes, Ralph}, title = {{Heterogeneous Substitution Systems Revisited}}, booktitle = {21st International Conference on Types for Proofs and Programs (TYPES 2015)}, pages = {2:1--2:23}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-030-9}, ISSN = {1868-8969}, year = {2018}, volume = {69}, editor = {Uustalu, Tarmo}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2015.2}, URN = {urn:nbn:de:0030-drops-84724}, doi = {10.4230/LIPIcs.TYPES.2015.2}, annote = {Keywords: formalization of category theory, nested datatypes, Mendler-style recursion schemes, representation of substitution in languages with variable binding} }
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} }
Feedback for Dagstuhl Publishing