Published in: OASIcs, Volume 109, Eelco Visser Commemorative Symposium (EVCS 2023)
Jan de Muijnck-Hughes, Guillaume Allais, and Edwin Brady. Type Theory as a Language Workbench. In Eelco Visser Commemorative Symposium (EVCS 2023). Open Access Series in Informatics (OASIcs), Volume 109, pp. 9:1-9:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
@InProceedings{demuijnckhughes_et_al:OASIcs.EVCS.2023.9, author = {de Muijnck-Hughes, Jan and Allais, Guillaume and Brady, Edwin}, title = {{Type Theory as a Language Workbench}}, booktitle = {Eelco Visser Commemorative Symposium (EVCS 2023)}, pages = {9:1--9:13}, series = {Open Access Series in Informatics (OASIcs)}, ISBN = {978-3-95977-267-9}, ISSN = {2190-6807}, year = {2023}, volume = {109}, editor = {L\"{a}mmel, Ralf and Mosses, Peter D. and Steimann, Friedrich}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.EVCS.2023.9}, URN = {urn:nbn:de:0030-drops-177797}, doi = {10.4230/OASIcs.EVCS.2023.9}, annote = {Keywords: dependent types, language workbenches, idris2, dsl, edsl, intrinsically scoped, well typed, co-De Bruijn} }
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} }
Published in: LIPIcs, Volume 104, 23rd International Conference on Types for Proofs and Programs (TYPES 2017)
Guillaume Allais. Typing with Leftovers - A mechanization of Intuitionistic Multiplicative-Additive Linear Logic. In 23rd International Conference on Types for Proofs and Programs (TYPES 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 104, pp. 1:1-1:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
@InProceedings{allais:LIPIcs.TYPES.2017.1, author = {Allais, Guillaume}, title = {{Typing with Leftovers - A mechanization of Intuitionistic Multiplicative-Additive Linear Logic}}, booktitle = {23rd International Conference on Types for Proofs and Programs (TYPES 2017)}, pages = {1:1--1:22}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-071-2}, ISSN = {1868-8969}, year = {2019}, volume = {104}, editor = {Abel, Andreas and Nordvall Forsberg, Fredrik and Kaposi, Ambrus}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2017.1}, URN = {urn:nbn:de:0030-drops-100490}, doi = {10.4230/LIPIcs.TYPES.2017.1}, annote = {Keywords: Type System, Bidirectional, Linear Logic, Agda} }
Published in: LIPIcs, Volume 15, 23rd International Conference on Rewriting Techniques and Applications (RTA'12) (2012)
René Thiemann, Guillaume Allais, and Julian Nagele. On the Formalization of Termination Techniques based on Multiset Orderings. In 23rd International Conference on Rewriting Techniques and Applications (RTA'12). Leibniz International Proceedings in Informatics (LIPIcs), Volume 15, pp. 339-354, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)
@InProceedings{thiemann_et_al:LIPIcs.RTA.2012.339, author = {Thiemann, Ren\'{e} and Allais, Guillaume and Nagele, Julian}, title = {{On the Formalization of Termination Techniques based on Multiset Orderings}}, booktitle = {23rd International Conference on Rewriting Techniques and Applications (RTA'12)}, pages = {339--354}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-38-5}, ISSN = {1868-8969}, year = {2012}, volume = {15}, editor = {Tiwari, Ashish}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2012.339}, URN = {urn:nbn:de:0030-drops-35029}, doi = {10.4230/LIPIcs.RTA.2012.339}, annote = {Keywords: formalization, term rewriting, termination, orderings} }
Feedback for Dagstuhl Publishing