28th International Conference on Types for Proofs and Programs (TYPES 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 269, pp. 1-342, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
@Proceedings{kesner_et_al:LIPIcs.TYPES.2022, title = {{LIPIcs, Volume 269, TYPES 2022, Complete Volume}}, booktitle = {28th International Conference on Types for Proofs and Programs (TYPES 2022)}, pages = {1--342}, 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}, URN = {urn:nbn:de:0030-drops-184425}, doi = {10.4230/LIPIcs.TYPES.2022}, annote = {Keywords: LIPIcs, Volume 269, TYPES 2022, Complete Volume} }
28th International Conference on Types for Proofs and Programs (TYPES 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 269, pp. 0:i-0:viii, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
@InProceedings{kesner_et_al:LIPIcs.TYPES.2022.0, author = {Kesner, Delia and P\'{e}drot, Pierre-Marie}, title = {{Front Matter, Table of Contents, Preface, Conference Organization}}, booktitle = {28th International Conference on Types for Proofs and Programs (TYPES 2022)}, pages = {0:i--0:viii}, 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.0}, URN = {urn:nbn:de:0030-drops-184433}, doi = {10.4230/LIPIcs.TYPES.2022.0}, annote = {Keywords: Front Matter, Table of Contents, Preface, Conference Organization} }
Dominic P. Mulligan. All Watched Over by Machines of Loving Grace. In 28th International Conference on Types for Proofs and Programs (TYPES 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 269, pp. 1:1-1:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
@InProceedings{mulligan:LIPIcs.TYPES.2022.1, author = {Mulligan, Dominic P.}, title = {{All Watched Over by Machines of Loving Grace}}, booktitle = {28th International Conference on Types for Proofs and Programs (TYPES 2022)}, pages = {1:1--1:23}, 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.1}, URN = {urn:nbn:de:0030-drops-184449}, doi = {10.4230/LIPIcs.TYPES.2022.1}, annote = {Keywords: Proof assistant design, operating systems, HOL, LCF, Supervisionary, system description, capabilities} }
Herman Geuvers and Tonny Hurkens. Classical Natural Deduction from Truth Tables. In 28th International Conference on Types for Proofs and Programs (TYPES 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 269, pp. 2:1-2:27, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
@InProceedings{geuvers_et_al:LIPIcs.TYPES.2022.2, author = {Geuvers, Herman and Hurkens, Tonny}, title = {{Classical Natural Deduction from Truth Tables}}, booktitle = {28th International Conference on Types for Proofs and Programs (TYPES 2022)}, pages = {2:1--2:27}, 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.2}, URN = {urn:nbn:de:0030-drops-184450}, doi = {10.4230/LIPIcs.TYPES.2022.2}, annote = {Keywords: Natural deduction, classical proposition logic, multiple conclusion natural deduction, proof terms, formulas-as-types, proof normalization, subformula property, Curry-Howard isomorphism} }
Andrea Colledan and Ugo Dal Lago. On Dynamic Lifting and Effect Typing in Circuit Description Languages. In 28th International Conference on Types for Proofs and Programs (TYPES 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 269, pp. 3:1-3:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
@InProceedings{colledan_et_al:LIPIcs.TYPES.2022.3, author = {Colledan, Andrea and Dal Lago, Ugo}, title = {{On Dynamic Lifting and Effect Typing in Circuit Description Languages}}, booktitle = {28th International Conference on Types for Proofs and Programs (TYPES 2022)}, pages = {3:1--3: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.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2022.3}, URN = {urn:nbn:de:0030-drops-184468}, doi = {10.4230/LIPIcs.TYPES.2022.3}, annote = {Keywords: Circuit-Description Languages, \lambda-calculus, Dynamic lifting, Type and effect systems} }
Emilie Grienenberger. Expressing Ecumenical Systems in the λΠ-Calculus Modulo Theory. In 28th International Conference on Types for Proofs and Programs (TYPES 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 269, pp. 4:1-4:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
@InProceedings{grienenberger:LIPIcs.TYPES.2022.4, author = {Grienenberger, Emilie}, title = {{Expressing Ecumenical Systems in the \lambda\Pi-Calculus Modulo Theory}}, booktitle = {28th International Conference on Types for Proofs and Programs (TYPES 2022)}, pages = {4:1--4:23}, 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.4}, URN = {urn:nbn:de:0030-drops-184479}, doi = {10.4230/LIPIcs.TYPES.2022.4}, annote = {Keywords: dependent types, predicate logic, higher order logic, constructivism, interoperability, ecumenical logics} }
Luca Padovani. On the Fair Termination of Client-Server Sessions. In 28th International Conference on Types for Proofs and Programs (TYPES 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 269, pp. 5:1-5:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
@InProceedings{padovani:LIPIcs.TYPES.2022.5, author = {Padovani, Luca}, title = {{On the Fair Termination of Client-Server Sessions}}, booktitle = {28th International Conference on Types for Proofs and Programs (TYPES 2022)}, pages = {5:1--5: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.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2022.5}, URN = {urn:nbn:de:0030-drops-184485}, doi = {10.4230/LIPIcs.TYPES.2022.5}, annote = {Keywords: client-server sessions, linear logic, fixed points, fair termination, cut elimination} }
Philipp Stassen, Daniel Gratzer, and Lars Birkedal. {mitten}: A Flexible Multimodal Proof Assistant. In 28th International Conference on Types for Proofs and Programs (TYPES 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 269, pp. 6:1-6:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
@InProceedings{stassen_et_al:LIPIcs.TYPES.2022.6, author = {Stassen, Philipp and Gratzer, Daniel and Birkedal, Lars}, title = {{\{mitten\}: A Flexible Multimodal Proof Assistant}}, booktitle = {28th International Conference on Types for Proofs and Programs (TYPES 2022)}, pages = {6:1--6:23}, 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.6}, URN = {urn:nbn:de:0030-drops-184498}, doi = {10.4230/LIPIcs.TYPES.2022.6}, annote = {Keywords: Dependent type theory, guarded recursion, modal type theory, proof assistants} }
Nathan Mull. An Irrelevancy-Eliminating Translation of Pure Type Systems. In 28th International Conference on Types for Proofs and Programs (TYPES 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 269, pp. 7:1-7:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
@InProceedings{mull:LIPIcs.TYPES.2022.7, author = {Mull, Nathan}, title = {{An Irrelevancy-Eliminating Translation of Pure Type Systems}}, booktitle = {28th International Conference on Types for Proofs and Programs (TYPES 2022)}, pages = {7:1--7: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.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2022.7}, URN = {urn:nbn:de:0030-drops-184501}, doi = {10.4230/LIPIcs.TYPES.2022.7}, annote = {Keywords: pure type systems, normalization, reduction-path-preserving translations, Barendregt-Geuvers-Klop conjecture} }
Fábio Reis, Sandra Alves, and Mário Florido. Linear Rank Intersection Types. In 28th International Conference on Types for Proofs and Programs (TYPES 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 269, pp. 8:1-8:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
@InProceedings{reis_et_al:LIPIcs.TYPES.2022.8, author = {Reis, F\'{a}bio and Alves, Sandra and Florido, M\'{a}rio}, title = {{Linear Rank Intersection Types}}, booktitle = {28th International Conference on Types for Proofs and Programs (TYPES 2022)}, pages = {8:1--8: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.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2022.8}, URN = {urn:nbn:de:0030-drops-184513}, doi = {10.4230/LIPIcs.TYPES.2022.8}, annote = {Keywords: Lambda-Calculus, Intersection Types, Quantitative Types, Tight Typings} }
Felix Bradley and Zhaohui Luo. A Metatheoretic Analysis of Subtype Universes. In 28th International Conference on Types for Proofs and Programs (TYPES 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 269, pp. 9:1-9:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
@InProceedings{bradley_et_al:LIPIcs.TYPES.2022.9, author = {Bradley, Felix and Luo, Zhaohui}, title = {{A Metatheoretic Analysis of Subtype Universes}}, booktitle = {28th International Conference on Types for Proofs and Programs (TYPES 2022)}, pages = {9:1--9: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.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2022.9}, URN = {urn:nbn:de:0030-drops-184520}, doi = {10.4230/LIPIcs.TYPES.2022.9}, annote = {Keywords: Type theory, coercive subtyping, subtype universes} }
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} }
Catherine Dubois, Nicolas Magaud, and Alain Giorgetti. Pragmatic Isomorphism Proofs Between Coq Representations: Application to Lambda-Term Families. In 28th International Conference on Types for Proofs and Programs (TYPES 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 269, pp. 11:1-11:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
@InProceedings{dubois_et_al:LIPIcs.TYPES.2022.11, author = {Dubois, Catherine and Magaud, Nicolas and Giorgetti, Alain}, title = {{Pragmatic Isomorphism Proofs Between Coq Representations: Application to Lambda-Term Families}}, booktitle = {28th International Conference on Types for Proofs and Programs (TYPES 2022)}, pages = {11:1--11:19}, 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.11}, URN = {urn:nbn:de:0030-drops-184548}, doi = {10.4230/LIPIcs.TYPES.2022.11}, annote = {Keywords: Data Representations, Isomorphisms, dependent Types, formal Proofs, random Generation, lambda Terms, Coq} }
Amélie Ledein, Valentin Blot, and Catherine Dubois. A Semantics of 𝕂 into Dedukti. In 28th International Conference on Types for Proofs and Programs (TYPES 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 269, pp. 12:1-12:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
@InProceedings{ledein_et_al:LIPIcs.TYPES.2022.12, author = {Ledein, Am\'{e}lie and Blot, Valentin and Dubois, Catherine}, title = {{A Semantics of \mathbb{K} into Dedukti}}, booktitle = {28th International Conference on Types for Proofs and Programs (TYPES 2022)}, pages = {12:1--12:22}, 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.12}, URN = {urn:nbn:de:0030-drops-184557}, doi = {10.4230/LIPIcs.TYPES.2022.12}, annote = {Keywords: Programming language, Semantics, Rewriting, Logical framework, Type theory} }
Marc Bezem, Thierry Coquand, Peter Dybjer, and Martín Escardó. Type Theory with Explicit Universe Polymorphism. In 28th International Conference on Types for Proofs and Programs (TYPES 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 269, pp. 13:1-13:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
@InProceedings{bezem_et_al:LIPIcs.TYPES.2022.13, author = {Bezem, Marc and Coquand, Thierry and Dybjer, Peter and Escard\'{o}, Mart{\'\i}n}, title = {{Type Theory with Explicit Universe Polymorphism}}, booktitle = {28th International Conference on Types for Proofs and Programs (TYPES 2022)}, pages = {13:1--13:16}, 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.13}, URN = {urn:nbn:de:0030-drops-184564}, doi = {10.4230/LIPIcs.TYPES.2022.13}, annote = {Keywords: type theory, universes in type theory, universe polymorphism, level-indexed products, constraint-indexed products} }
Max Zeuner and Anders Mörtberg. A Univalent Formalization of Constructive Affine Schemes. In 28th International Conference on Types for Proofs and Programs (TYPES 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 269, pp. 14:1-14:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
@InProceedings{zeuner_et_al:LIPIcs.TYPES.2022.14, author = {Zeuner, Max and M\"{o}rtberg, Anders}, title = {{A Univalent Formalization of Constructive Affine Schemes}}, booktitle = {28th International Conference on Types for Proofs and Programs (TYPES 2022)}, pages = {14:1--14:24}, 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.14}, URN = {urn:nbn:de:0030-drops-184574}, doi = {10.4230/LIPIcs.TYPES.2022.14}, annote = {Keywords: Affine Schemes, Homotopy Type Theory and Univalent Foundations, Cubical Agda, Constructive Mathematics} }
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.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} }