Published in: LIPIcs, Volume 303, 29th International Conference on Types for Proofs and Programs (TYPES 2023)
Joris Ceulemans, Andreas Nuyts, and Dominique Devriese. A Sound and Complete Substitution Algorithm for Multimode Type Theory. In 29th International Conference on Types for Proofs and Programs (TYPES 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 303, pp. 4:1-4:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{ceulemans_et_al:LIPIcs.TYPES.2023.4, author = {Ceulemans, Joris and Nuyts, Andreas and Devriese, Dominique}, title = {{A Sound and Complete Substitution Algorithm for Multimode Type Theory}}, booktitle = {29th International Conference on Types for Proofs and Programs (TYPES 2023)}, pages = {4:1--4:23}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-332-4}, ISSN = {1868-8969}, year = {2024}, volume = {303}, editor = {Kesner, Delia and Reyes, Eduardo Hermo and van den Berg, Benno}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2023.4}, URN = {urn:nbn:de:0030-drops-204826}, doi = {10.4230/LIPIcs.TYPES.2023.4}, annote = {Keywords: dependent type theory, modalities, multimode type theory, explicit substitutions, substitution algorithm} }
Published in: LIPIcs, Volume 299, 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)
Niels van der Weide. Univalent Enriched Categories and the Enriched Rezk Completion. In 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 299, pp. 4:1-4:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{vanderweide:LIPIcs.FSCD.2024.4, author = {van der Weide, Niels}, title = {{Univalent Enriched Categories and the Enriched Rezk Completion}}, booktitle = {9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)}, pages = {4:1--4:19}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-323-2}, ISSN = {1868-8969}, year = {2024}, volume = {299}, editor = {Rehof, Jakob}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2024.4}, URN = {urn:nbn:de:0030-drops-203337}, doi = {10.4230/LIPIcs.FSCD.2024.4}, annote = {Keywords: enriched categories, univalent categories, homotopy type theory, univalent foundations, Rezk completion} }
Published in: LIPIcs, Volume 299, 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)
Małgorzata Biernacka, Dariusz Biernacki, Sergueï Lenglet, and Alan Schmitt. Optimizing a Non-Deterministic Abstract Machine with Environments. In 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 299, pp. 11:1-11:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{biernacka_et_al:LIPIcs.FSCD.2024.11, author = {Biernacka, Ma{\l}gorzata and Biernacki, Dariusz and Lenglet, Sergue\"{i} and Schmitt, Alan}, title = {{Optimizing a Non-Deterministic Abstract Machine with Environments}}, booktitle = {9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)}, pages = {11:1--11:22}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-323-2}, ISSN = {1868-8969}, year = {2024}, volume = {299}, editor = {Rehof, Jakob}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2024.11}, URN = {urn:nbn:de:0030-drops-203409}, doi = {10.4230/LIPIcs.FSCD.2024.11}, annote = {Keywords: Abstract machine, Explicit substitutions, Refocusing} }
Published in: LIPIcs, Volume 299, 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)
Kostia Chardonnet, Louis Lemonnier, and Benoît Valiron. Semantics for a Turing-Complete Reversible Programming Language with Inductive Types. In 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 299, pp. 19:1-19:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{chardonnet_et_al:LIPIcs.FSCD.2024.19, author = {Chardonnet, Kostia and Lemonnier, Louis and Valiron, Beno\^{i}t}, title = {{Semantics for a Turing-Complete Reversible Programming Language with Inductive Types}}, booktitle = {9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)}, pages = {19:1--19:19}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-323-2}, ISSN = {1868-8969}, year = {2024}, volume = {299}, editor = {Rehof, Jakob}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2024.19}, URN = {urn:nbn:de:0030-drops-203487}, doi = {10.4230/LIPIcs.FSCD.2024.19}, annote = {Keywords: Reversible programming, functional programming, Computability, Denotational Semantics} }
Published in: LIPIcs, Volume 299, 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)
Beniamino Accattoli and Claudio Sacerdoti Coen. IMELL Cut Elimination with Linear Overhead. In 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 299, pp. 24:1-24:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{accattoli_et_al:LIPIcs.FSCD.2024.24, author = {Accattoli, Beniamino and Sacerdoti Coen, Claudio}, title = {{IMELL Cut Elimination with Linear Overhead}}, booktitle = {9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)}, pages = {24:1--24:24}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-323-2}, ISSN = {1868-8969}, year = {2024}, volume = {299}, editor = {Rehof, Jakob}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2024.24}, URN = {urn:nbn:de:0030-drops-203539}, doi = {10.4230/LIPIcs.FSCD.2024.24}, annote = {Keywords: Lambda calculus, linear logic, abstract machines} }
Published in: LIPIcs, Volume 268, 14th International Conference on Interactive Theorem Proving (ITP 2023)
Philipp Joram and Niccolò Veltri. Constructive Final Semantics of Finite Bags. In 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, pp. 20:1-20:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
@InProceedings{joram_et_al:LIPIcs.ITP.2023.20, author = {Joram, Philipp and Veltri, Niccol\`{o}}, title = {{Constructive Final Semantics of Finite Bags}}, booktitle = {14th International Conference on Interactive Theorem Proving (ITP 2023)}, pages = {20:1--20:19}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-284-6}, ISSN = {1868-8969}, year = {2023}, volume = {268}, editor = {Naumowicz, Adam and Thiemann, Ren\'{e}}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2023.20}, URN = {urn:nbn:de:0030-drops-183954}, doi = {10.4230/LIPIcs.ITP.2023.20}, annote = {Keywords: finite bags, final coalgebra, homotopy type theory, Cubical Agda} }
Published in: LIPIcs, Volume 222, 36th European Conference on Object-Oriented Programming (ECOOP 2022)
Danielle Marshall and Dominic Orchard. How to Take the Inverse of a Type. In 36th European Conference on Object-Oriented Programming (ECOOP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 222, pp. 5:1-5:27, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
@InProceedings{marshall_et_al:LIPIcs.ECOOP.2022.5, author = {Marshall, Danielle and Orchard, Dominic}, title = {{How to Take the Inverse of a Type}}, booktitle = {36th European Conference on Object-Oriented Programming (ECOOP 2022)}, pages = {5:1--5:27}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-225-9}, ISSN = {1868-8969}, year = {2022}, volume = {222}, editor = {Ali, Karim and Vitek, Jan}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2022.5}, URN = {urn:nbn:de:0030-drops-162339}, doi = {10.4230/LIPIcs.ECOOP.2022.5}, annote = {Keywords: linear types, regular types, algebra of programming, derivatives} }
Published in: LIPIcs, Volume 195, 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)
Niccolò Veltri. Type-Theoretic Constructions of the Final Coalgebra of the Finite Powerset Functor. In 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 195, pp. 22:1-22:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
@InProceedings{veltri:LIPIcs.FSCD.2021.22, author = {Veltri, Niccol\`{o}}, title = {{Type-Theoretic Constructions of the Final Coalgebra of the Finite Powerset Functor}}, booktitle = {6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)}, pages = {22:1--22:18}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-191-7}, ISSN = {1868-8969}, year = {2021}, volume = {195}, editor = {Kobayashi, Naoki}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2021.22}, URN = {urn:nbn:de:0030-drops-142601}, doi = {10.4230/LIPIcs.FSCD.2021.22}, annote = {Keywords: type theory, finite powerset, final coalgebra, Cubical Agda} }
Published in: LIPIcs, Volume 131, 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)
Benedikt Ahrens, Dan Frumin, Marco Maggesi, and Niels van der Weide. Bicategories in Univalent Foundations. In 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 131, pp. 5:1-5:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
@InProceedings{ahrens_et_al:LIPIcs.FSCD.2019.5, author = {Ahrens, Benedikt and Frumin, Dan and Maggesi, Marco and van der Weide, Niels}, title = {{Bicategories in Univalent Foundations}}, booktitle = {4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)}, pages = {5:1--5:17}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-107-8}, ISSN = {1868-8969}, year = {2019}, volume = {131}, editor = {Geuvers, Herman}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2019.5}, URN = {urn:nbn:de:0030-drops-105124}, doi = {10.4230/LIPIcs.FSCD.2019.5}, annote = {Keywords: bicategory theory, univalent mathematics, dependent type theory, Coq} }
Published in: LIPIcs, Volume 131, 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)
Niccolò Veltri and Niels van der Weide. Guarded Recursion in Agda via Sized Types. In 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 131, pp. 32:1-32:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
@InProceedings{veltri_et_al:LIPIcs.FSCD.2019.32, author = {Veltri, Niccol\`{o} and van der Weide, Niels}, title = {{Guarded Recursion in Agda via Sized Types}}, booktitle = {4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)}, pages = {32:1--32:19}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-107-8}, ISSN = {1868-8969}, year = {2019}, volume = {131}, editor = {Geuvers, Herman}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2019.32}, URN = {urn:nbn:de:0030-drops-105391}, doi = {10.4230/LIPIcs.FSCD.2019.32}, annote = {Keywords: guarded recursion, type theory, semantics, coinduction, sized types} }
Feedback for Dagstuhl Publishing