LIPIcs, Volume 188
TYPES 2020, March 2-5, 2020, University of Turin, Italy
Editors: Ugo de'Liguoro, Stefano Berardi, and Thorsten Altenkirch
LIPIcs, Volume 38
TLCA 2015, July 1-3, 2015, Warsaw, Poland
Editors: Thorsten Altenkirch
Published in: LIPIcs, Volume 269, 28th International Conference on Types for Proofs and Programs (TYPES 2022)
Thorsten Altenkirch, Ambrus Kaposi, Artjoms Šinkarovs, and Tamás Végh. The Münchhausen Method in Type Theory. In 28th International Conference on Types for Proofs and Programs (TYPES 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 269, pp. 10:1-10:20, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2023)
@InProceedings{altenkirch_et_al:LIPIcs.TYPES.2022.10, author = {Altenkirch, Thorsten and Kaposi, Ambrus and \v{S}inkarovs, Artjoms and V\'{e}gh, Tam\'{a}s}, title = {{The M\"{u}nchhausen Method in Type Theory}}, booktitle = {28th International Conference on Types for Proofs and Programs (TYPES 2022)}, pages = {10:1--10:20}, 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.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2022.10}, URN = {urn:nbn:de:0030-drops-184534}, doi = {10.4230/LIPIcs.TYPES.2022.10}, annote = {Keywords: type theory, proof assistants, very dependent types} }
Published in: LIPIcs, Volume 260, 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)
Thorsten Altenkirch, Ambrus Kaposi, Artjoms Šinkarovs, and Tamás Végh. Combinatory Logic and Lambda Calculus Are Equal, Algebraically. In 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 260, pp. 24:1-24:19, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2023)
@InProceedings{altenkirch_et_al:LIPIcs.FSCD.2023.24, author = {Altenkirch, Thorsten and Kaposi, Ambrus and \v{S}inkarovs, Artjoms and V\'{e}gh, Tam\'{a}s}, title = {{Combinatory Logic and Lambda Calculus Are Equal, Algebraically}}, booktitle = {8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)}, pages = {24:1--24:19}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-277-8}, ISSN = {1868-8969}, year = {2023}, volume = {260}, editor = {Gaboardi, Marco and van Raamsdonk, Femke}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2023.24}, URN = {urn:nbn:de:0030-drops-180086}, doi = {10.4230/LIPIcs.FSCD.2023.24}, annote = {Keywords: Combinatory logic, lambda calculus, quotient inductive types, Cubical Agda} }
Published in: LIPIcs, Volume 202, 46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021)
Nicolai Kraus, Fredrik Nordvall Forsberg, and Chuangjie Xu. Connecting Constructive Notions of Ordinals in Homotopy Type Theory. In 46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 202, pp. 70:1-70:16, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2021)
@InProceedings{kraus_et_al:LIPIcs.MFCS.2021.70, author = {Kraus, Nicolai and Nordvall Forsberg, Fredrik and Xu, Chuangjie}, title = {{Connecting Constructive Notions of Ordinals in Homotopy Type Theory}}, booktitle = {46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021)}, pages = {70:1--70:16}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-201-3}, ISSN = {1868-8969}, year = {2021}, volume = {202}, editor = {Bonchi, Filippo and Puglisi, Simon J.}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2021.70}, URN = {urn:nbn:de:0030-drops-145100}, doi = {10.4230/LIPIcs.MFCS.2021.70}, annote = {Keywords: Constructive ordinals, Cantor normal forms, Brouwer trees} }
Published in: LIPIcs, Volume 188, 26th International Conference on Types for Proofs and Programs (TYPES 2020)
Ugo de'Liguoro, Stefano Berardi, and Thorsten Altenkirch. LIPIcs, Volume 188, TYPES 2020, Complete Volume. In 26th International Conference on Types for Proofs and Programs (TYPES 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 188, pp. 1-204, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2021)
@Proceedings{deliguoro_et_al:LIPIcs.TYPES.2020, title = {{LIPIcs, Volume 188, TYPES 2020, Complete Volume}}, booktitle = {26th International Conference on Types for Proofs and Programs (TYPES 2020)}, pages = {1--204}, 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.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2020}, URN = {urn:nbn:de:0030-drops-138785}, doi = {10.4230/LIPIcs.TYPES.2020}, annote = {Keywords: LIPIcs, Volume 188, TYPES 2020, Complete Volume} }
Published in: LIPIcs, Volume 188, 26th International Conference on Types for Proofs and Programs (TYPES 2020)
Ugo de'Liguoro, Stefano Berardi, and Thorsten Altenkirch. Front Matter, Table of Contents, Preface, Conference Organization. In 26th International Conference on Types for Proofs and Programs (TYPES 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 188, pp. 0:i-0:viii, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2021)
@InProceedings{deliguoro_et_al:LIPIcs.TYPES.2020.0, author = {de'Liguoro, Ugo and Berardi, Stefano and Altenkirch, Thorsten}, title = {{Front Matter, Table of Contents, Preface, Conference Organization}}, booktitle = {26th International Conference on Types for Proofs and Programs (TYPES 2020)}, pages = {0:i--0:viii}, 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.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2020.0}, URN = {urn:nbn:de:0030-drops-138792}, doi = {10.4230/LIPIcs.TYPES.2020.0}, annote = {Keywords: Front Matter, Table of Contents, Preface, Conference Organization} }
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.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)
Reynald Affeldt and David Nowak. Extending Equational Monadic Reasoning with Monad Transformers. In 26th International Conference on Types for Proofs and Programs (TYPES 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 188, pp. 2:1-2:21, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2021)
@InProceedings{affeldt_et_al:LIPIcs.TYPES.2020.2, author = {Affeldt, Reynald and Nowak, David}, title = {{Extending Equational Monadic Reasoning with Monad Transformers}}, booktitle = {26th International Conference on Types for Proofs and Programs (TYPES 2020)}, pages = {2:1--2: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.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2020.2}, URN = {urn:nbn:de:0030-drops-138810}, doi = {10.4230/LIPIcs.TYPES.2020.2}, annote = {Keywords: monads, monad transformers, Coq, impredicativity, parametricity} }
Published in: LIPIcs, Volume 188, 26th International Conference on Types for Proofs and Programs (TYPES 2020)
Guido De Luca and Carlos Luna. Towards a Certified Reference Monitor of the Android 10 Permission System. In 26th International Conference on Types for Proofs and Programs (TYPES 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 188, pp. 3:1-3:18, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2021)
@InProceedings{deluca_et_al:LIPIcs.TYPES.2020.3, author = {De Luca, Guido and Luna, Carlos}, title = {{Towards a Certified Reference Monitor of the Android 10 Permission System}}, booktitle = {26th International Conference on Types for Proofs and Programs (TYPES 2020)}, pages = {3:1--3:18}, 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.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2020.3}, URN = {urn:nbn:de:0030-drops-138821}, doi = {10.4230/LIPIcs.TYPES.2020.3}, annote = {Keywords: Android, Permission model, Formal idealized model, Reference monitor, Formal proofs, Certified implementation, Coq} }
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.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 188, 26th International Conference on Types for Proofs and Programs (TYPES 2020)
Asta Halkjær From. Synthetic Completeness for a Terminating Seligman-Style Tableau System. In 26th International Conference on Types for Proofs and Programs (TYPES 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 188, pp. 5:1-5:17, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2021)
@InProceedings{from:LIPIcs.TYPES.2020.5, author = {From, Asta Halkj{\ae}r}, title = {{Synthetic Completeness for a Terminating Seligman-Style Tableau System}}, booktitle = {26th International Conference on Types for Proofs and Programs (TYPES 2020)}, pages = {5:1--5:17}, 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.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2020.5}, URN = {urn:nbn:de:0030-drops-138847}, doi = {10.4230/LIPIcs.TYPES.2020.5}, annote = {Keywords: Hybrid logic, Seligman-style tableau, synthetic completeness, Isabelle/HOL} }
Published in: LIPIcs, Volume 188, 26th International Conference on Types for Proofs and Programs (TYPES 2020)
Gabriel Hondet and Frédéric Blanqui. Encoding of Predicate Subtyping with Proof Irrelevance in the λΠ-Calculus Modulo Theory. In 26th International Conference on Types for Proofs and Programs (TYPES 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 188, pp. 6:1-6:18, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2021)
@InProceedings{hondet_et_al:LIPIcs.TYPES.2020.6, author = {Hondet, Gabriel and Blanqui, Fr\'{e}d\'{e}ric}, title = {{Encoding of Predicate Subtyping with Proof Irrelevance in the \lambda\Pi-Calculus Modulo Theory}}, booktitle = {26th International Conference on Types for Proofs and Programs (TYPES 2020)}, pages = {6:1--6:18}, 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.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2020.6}, URN = {urn:nbn:de:0030-drops-138853}, doi = {10.4230/LIPIcs.TYPES.2020.6}, annote = {Keywords: Predicate Subtyping, Logical Framework, PVS, Dedukti, Proof Irrelevance} }
Published in: LIPIcs, Volume 188, 26th International Conference on Types for Proofs and Programs (TYPES 2020)
Furio Honsell, Marina Lenisa, and Ivan Scagnetto. Λ-Symsym: An Interactive Tool for Playing with Involutions and Types. In 26th International Conference on Types for Proofs and Programs (TYPES 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 188, pp. 7:1-7:18, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2021)
@InProceedings{honsell_et_al:LIPIcs.TYPES.2020.7, author = {Honsell, Furio and Lenisa, Marina and Scagnetto, Ivan}, title = {{\Lambda-Symsym: An Interactive Tool for Playing with Involutions and Types}}, booktitle = {26th International Conference on Types for Proofs and Programs (TYPES 2020)}, pages = {7:1--7:18}, 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.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2020.7}, URN = {urn:nbn:de:0030-drops-138867}, doi = {10.4230/LIPIcs.TYPES.2020.7}, annote = {Keywords: game semantics, lambda calculus, involutions, linear logic, implicit computational complexity} }
Published in: LIPIcs, Volume 188, 26th International Conference on Types for Proofs and Programs (TYPES 2020)
Jasper Hugunin. Why Not W?. In 26th International Conference on Types for Proofs and Programs (TYPES 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 188, pp. 8:1-8:9, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2021)
@InProceedings{hugunin:LIPIcs.TYPES.2020.8, author = {Hugunin, Jasper}, title = {{Why Not W?}}, booktitle = {26th International Conference on Types for Proofs and Programs (TYPES 2020)}, pages = {8:1--8:9}, 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.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2020.8}, URN = {urn:nbn:de:0030-drops-138876}, doi = {10.4230/LIPIcs.TYPES.2020.8}, annote = {Keywords: dependent types, intensional type theory, inductive types, W types} }
Feedback for Dagstuhl Publishing