LIPIcs, Volume 269
TYPES 2022, June 20-25, 2022, LS2N, University of Nantes, France
Editors: Delia Kesner and Pierre-Marie Pédrot
LIPIcs, Volume 52
FSCD 2016, June 22-26, 2016, Porto, Portugal
Editors: Delia Kesner and Brigitte Pientka
Published in: LIPIcs, Volume 270, 10th Conference on Algebra and Coalgebra in Computer Science (CALCO 2023)
Elaine Pimentel and Luiz Carlos Pereira. A Tour on Ecumenical Systems (Invited Talk). In 10th Conference on Algebra and Coalgebra in Computer Science (CALCO 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 270, pp. 3:1-3:15, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2023)
@InProceedings{pimentel_et_al:LIPIcs.CALCO.2023.3, author = {Pimentel, Elaine and Pereira, Luiz Carlos}, title = {{A Tour on Ecumenical Systems}}, booktitle = {10th Conference on Algebra and Coalgebra in Computer Science (CALCO 2023)}, pages = {3:1--3:15}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-287-7}, ISSN = {1868-8969}, year = {2023}, volume = {270}, editor = {Baldan, Paolo and de Paiva, Valeria}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2023.3}, URN = {urn:nbn:de:0030-drops-188003}, doi = {10.4230/LIPIcs.CALCO.2023.3}, annote = {Keywords: Intuitionistic logic, classical logic, modal logic, ecumenical systems, proof theory} }
Published in: LIPIcs, Volume 269, 28th International Conference on Types for Proofs and Programs (TYPES 2022)
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} }
Published in: LIPIcs, Volume 269, 28th International Conference on Types for Proofs and Programs (TYPES 2022)
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} }
Published in: LIPIcs, Volume 269, 28th International Conference on Types for Proofs and Programs (TYPES 2022)
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} }
Published in: LIPIcs, Volume 269, 28th International Conference on Types for Proofs and Programs (TYPES 2022)
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} }
Published in: LIPIcs, Volume 269, 28th International Conference on Types for Proofs and Programs (TYPES 2022)
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} }
Published in: LIPIcs, Volume 269, 28th International Conference on Types for Proofs and Programs (TYPES 2022)
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} }
Published in: LIPIcs, Volume 269, 28th International Conference on Types for Proofs and Programs (TYPES 2022)
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} }
Published in: LIPIcs, Volume 269, 28th International Conference on Types for Proofs and Programs (TYPES 2022)
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} }
Published in: LIPIcs, Volume 269, 28th International Conference on Types for Proofs and Programs (TYPES 2022)
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} }
Published in: LIPIcs, Volume 269, 28th International Conference on Types for Proofs and Programs (TYPES 2022)
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} }
Published in: LIPIcs, Volume 269, 28th International Conference on Types for Proofs and Programs (TYPES 2022)
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} }
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} }
Feedback for Dagstuhl Publishing