@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}
}
@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}
}
@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}
}
@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}
}
@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}
}
@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}
}
@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}
}
@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}
}
@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}
}
@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}
}
@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}
}
@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}
}
@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}
}
@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}
}
@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}
}
@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}
}
@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}
}
The metadata provided by Dagstuhl Publishing on its webpages, as well as their export formats (such as XML or BibTeX) available at our website, is released under the CC0 1.0 Public Domain Dedication license. That is, you are free to copy, distribute, use, modify, transform, build upon, and produce derived works from our data, even for commercial purposes, all without asking permission. Of course, we are always happy if you provide a link to us as the source of the data.
Read the full CC0 1.0 legal code for the exact terms that apply: https://creativecommons.org/publicdomain/zero/1.0/legalcode
Feedback for Dagstuhl Publishing