Published in: LIPIcs, Volume 216, 30th EACSL Annual Conference on Computer Science Logic (CSL 2022)
Liang-Ting Chen and Hsiang-Shang Ko. Realising Intensional S4 and GL Modalities. In 30th EACSL Annual Conference on Computer Science Logic (CSL 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 216, pp. 14:1-14:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
@InProceedings{chen_et_al:LIPIcs.CSL.2022.14, author = {Chen, Liang-Ting and Ko, Hsiang-Shang}, title = {{Realising Intensional S4 and GL Modalities}}, booktitle = {30th EACSL Annual Conference on Computer Science Logic (CSL 2022)}, pages = {14:1--14:17}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-218-1}, ISSN = {1868-8969}, year = {2022}, volume = {216}, editor = {Manea, Florin and Simpson, Alex}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2022.14}, URN = {urn:nbn:de:0030-drops-157341}, doi = {10.4230/LIPIcs.CSL.2022.14}, annote = {Keywords: provability, guarded recursion, realisability, modal types, metaprogramming} }
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-dev.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 175, 25th International Conference on Types for Proofs and Programs (TYPES 2019)
Nils Anders Danielsson. Higher Inductive Type Eliminators Without Paths. In 25th International Conference on Types for Proofs and Programs (TYPES 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 175, pp. 10:1-10:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
@InProceedings{danielsson:LIPIcs.TYPES.2019.10, author = {Danielsson, Nils Anders}, title = {{Higher Inductive Type Eliminators Without Paths}}, booktitle = {25th International Conference on Types for Proofs and Programs (TYPES 2019)}, pages = {10:1--10:18}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-158-0}, ISSN = {1868-8969}, year = {2020}, volume = {175}, editor = {Bezem, Marc and Mahboubi, Assia}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2019.10}, URN = {urn:nbn:de:0030-drops-130749}, doi = {10.4230/LIPIcs.TYPES.2019.10}, annote = {Keywords: Cubical Agda, higher inductive types} }
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-dev.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} }
Published in: LIPIcs, Volume 62, 25th EACSL Annual Conference on Computer Science Logic (CSL 2016)
Lars Birkedal, Aleš Bizjak, Ranald Clouston, Hans Bugge Grathwohl, Bas Spitters, and Andrea Vezzosi. Guarded Cubical Type Theory: Path Equality for Guarded Recursion. In 25th EACSL Annual Conference on Computer Science Logic (CSL 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 62, pp. 23:1-23:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
@InProceedings{birkedal_et_al:LIPIcs.CSL.2016.23, author = {Birkedal, Lars and Bizjak, Ale\v{s} and Clouston, Ranald and Grathwohl, Hans Bugge and Spitters, Bas and Vezzosi, Andrea}, title = {{Guarded Cubical Type Theory: Path Equality for Guarded Recursion}}, booktitle = {25th EACSL Annual Conference on Computer Science Logic (CSL 2016)}, pages = {23:1--23:17}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-022-4}, ISSN = {1868-8969}, year = {2016}, volume = {62}, editor = {Talbot, Jean-Marc and Regnier, Laurent}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2016.23}, URN = {urn:nbn:de:0030-drops-65638}, doi = {10.4230/LIPIcs.CSL.2016.23}, annote = {Keywords: Guarded Recursion, Dependent Type Theory, Cubical Type Theory, Denotational Semantics, Homotopy Type Theory} }
Published in: LIPIcs, Volume 41, 24th EACSL Annual Conference on Computer Science Logic (CSL 2015)
Paolo Capriotti, Nicolai Kraus, and Andrea Vezzosi. Functions out of Higher Truncations. In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 41, pp. 359-373, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
@InProceedings{capriotti_et_al:LIPIcs.CSL.2015.359, author = {Capriotti, Paolo and Kraus, Nicolai and Vezzosi, Andrea}, title = {{Functions out of Higher Truncations}}, booktitle = {24th EACSL Annual Conference on Computer Science Logic (CSL 2015)}, pages = {359--373}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-90-3}, ISSN = {1868-8969}, year = {2015}, volume = {41}, editor = {Kreutzer, Stephan}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2015.359}, URN = {urn:nbn:de:0030-drops-54257}, doi = {10.4230/LIPIcs.CSL.2015.359}, annote = {Keywords: homotopy type theory, truncation elimination, constancy on loop spaces} }
Feedback for Dagstuhl Publishing