Published in: LIPIcs, Volume 193, 12th International Conference on Interactive Theorem Proving (ITP 2021)
Meven Lennon-Bertrand. Complete Bidirectional Typing for the Calculus of Inductive Constructions. In 12th International Conference on Interactive Theorem Proving (ITP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 193, pp. 24:1-24:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
@InProceedings{lennonbertrand:LIPIcs.ITP.2021.24, author = {Lennon-Bertrand, Meven}, title = {{Complete Bidirectional Typing for the Calculus of Inductive Constructions}}, booktitle = {12th International Conference on Interactive Theorem Proving (ITP 2021)}, pages = {24:1--24:19}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-188-7}, ISSN = {1868-8969}, year = {2021}, volume = {193}, editor = {Cohen, Liron and Kaliszyk, Cezary}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2021.24}, URN = {urn:nbn:de:0030-drops-139194}, doi = {10.4230/LIPIcs.ITP.2021.24}, annote = {Keywords: Bidirectional Typing, Calculus of Inductive Constructions, Coq, Proof Assistants} }
Published in: LIPIcs, Volume 39, 20th International Conference on Types for Proofs and Programs (TYPES 2014)
Olivier Danvy, Chantal Keller, and Matthias Puech. Typeful Normalization by Evaluation. In 20th International Conference on Types for Proofs and Programs (TYPES 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 39, pp. 72-88, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
@InProceedings{danvy_et_al:LIPIcs.TYPES.2014.72, author = {Danvy, Olivier and Keller, Chantal and Puech, Matthias}, title = {{Typeful Normalization by Evaluation}}, booktitle = {20th International Conference on Types for Proofs and Programs (TYPES 2014)}, pages = {72--88}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-88-0}, ISSN = {1868-8969}, year = {2015}, volume = {39}, editor = {Herbelin, Hugo and Letouzey, Pierre and Sozeau, Matthieu}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2014.72}, URN = {urn:nbn:de:0030-drops-54921}, doi = {10.4230/LIPIcs.TYPES.2014.72}, annote = {Keywords: Normalization by Evaluation, Generalized Algebraic Data Types, Continuation-Passing Style, partial evaluation} }
Published in: LIPIcs, Volume 16, Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL (2012)
Chantal Keller and Marc Lasson. Parametricity in an Impredicative Sort. In Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Volume 16, pp. 381-395, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)
@InProceedings{keller_et_al:LIPIcs.CSL.2012.381, author = {Keller, Chantal and Lasson, Marc}, title = {{Parametricity in an Impredicative Sort}}, booktitle = {Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL}, pages = {381--395}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-42-2}, ISSN = {1868-8969}, year = {2012}, volume = {16}, editor = {C\'{e}gielski, Patrick and Durand, Arnaud}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2012.381}, URN = {urn:nbn:de:0030-drops-36851}, doi = {10.4230/LIPIcs.CSL.2012.381}, annote = {Keywords: Calculus of Inductive Constructions, parametricity, impredicativity, Coq, universes} }
Feedback for Dagstuhl Publishing