3 Search Results for "Keller, Chantal"


Document
Complete Bidirectional Typing for the Calculus of Inductive Constructions

Authors: Meven Lennon-Bertrand

Published in: LIPIcs, Volume 193, 12th International Conference on Interactive Theorem Proving (ITP 2021)


Abstract
This article presents a bidirectional type system for the Calculus of Inductive Constructions (CIC). The key property of the system is its completeness with respect to the usual undirected one, which has been formally proven in Coq as a part of the MetaCoq project. Although it plays an important role in an ongoing completeness proof for a realistic typing algorithm, the interest of bidirectionality is wider, as it gives insights and structure when trying to prove properties on CIC or design variations and extensions. In particular, we put forward constrained inference, an intermediate between the usual inference and checking judgements, to handle the presence of computation in types.

Cite as

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)


Copy BibTex To Clipboard

@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}
}
Document
Typeful Normalization by Evaluation

Authors: Olivier Danvy, Chantal Keller, and Matthias Puech

Published in: LIPIcs, Volume 39, 20th International Conference on Types for Proofs and Programs (TYPES 2014)


Abstract
We present the first typeful implementation of Normalization by Evaluation for the simply typed lambda-calculus with sums and control operators: we guarantee type preservation and eta-long (modulo commuting conversions), beta-normal forms using only Generalized Algebraic Data Types in a general-purpose programming language, here OCaml; and we account for sums and control operators with Continuation-Passing Style. First, we implement the standard NbE algorithm for the implicational fragment in a typeful way that is correct by construction. We then derive its call-by-value continuation-passing counterpart, that maps a lambda-term with sums and call/cc into a CPS term in normal form, which we express in a typed dedicated syntax. Beyond showcasing the expressive power of GADTs, we emphasize that type inference gives a smooth way to re-derive the encodings of the syntax and typing of normal forms in Continuation-Passing Style.

Cite as

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)


Copy BibTex To Clipboard

@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}
}
Document
Parametricity in an Impredicative Sort

Authors: Chantal Keller and Marc Lasson

Published in: LIPIcs, Volume 16, Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL (2012)


Abstract
Reynold's abstraction theorem is now a well-established result for a large class of type systems. We propose here a definition of relational parametricity and a proof of the abstraction theorem in the Calculus of Inductive Constructions (CIC), the underlying formal language of Coq, in which parametricity relations' codomain is the impredicative sort of propositions. To proceed, we need to refine this calculus by splitting the sort hierarchy to separate informative terms from non-informative terms. This refinement is very close to CIC, but with the property that typing judgments can distinguish informative terms. Among many applications, this natural encoding of parametricity inside CIC serves both theoretical purposes (proving the independence of propositions with respect to the logical system) as well as practical aspirations (proving properties of finite algebraic structures). We finally discuss how we can simply build, on top of our calculus, a new reflexive Coq tactic that constructs proof terms by parametricity.

Cite as

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)


Copy BibTex To Clipboard

@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}
}
  • Refine by Author
  • 2 Keller, Chantal
  • 1 Danvy, Olivier
  • 1 Lasson, Marc
  • 1 Lennon-Bertrand, Meven
  • 1 Puech, Matthias

  • Refine by Classification
  • 1 Theory of computation → Type theory

  • Refine by Keyword
  • 2 Calculus of Inductive Constructions
  • 2 Coq
  • 1 Bidirectional Typing
  • 1 Continuation-Passing Style
  • 1 Generalized Algebraic Data Types
  • Show More...

  • Refine by Type
  • 3 document

  • Refine by Publication Year
  • 1 2012
  • 1 2015
  • 1 2021

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail