6 Search Results for "Tabareau, Nicolas"

Document
DOI: 10.4230/LIPIcs.ITP.2024.26
The Rewster: Type Preserving Rewrite Rules for the Coq Proof Assistant

Authors: Yann Leray, Gaëtan Gilbert, Nicolas Tabareau, and Théo Winterhalter

Published in: LIPIcs, Volume 309, 15th International Conference on Interactive Theorem Proving (ITP 2024)

Abstract
In dependently typed proof assistants, users can declare axioms to extend the ambient logic locally with new principles and propositional equalities governing them. Additionally, rewrite rules have recently been proposed to allow users to extend the logic with new definitional equalities, enabling them to handle new principles with a computational behaviour. While axioms can only break consistency, the addition of arbitrary rewrite rules can break other important metatheoretical properties such as type preservation. In this paper, we present an implementation of rewrite rules on top of the Coq proof assistant, together with a modular criterion to ensure that the added rewrite rules preserve typing. This criterion, based on bidirectional type checking, is formally expressed in PCUIC - the type theory of Coq recently developed in the MetaCoq project.
Cite as

Yann Leray, Gaëtan Gilbert, Nicolas Tabareau, and Théo Winterhalter. The Rewster: Type Preserving Rewrite Rules for the Coq Proof Assistant. In 15th International Conference on Interactive Theorem Proving (ITP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 309, pp. 26:1-26:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{leray_et_al:LIPIcs.ITP.2024.26,
  author =	{Leray, Yann and Gilbert, Ga\"{e}tan and Tabareau, Nicolas and Winterhalter, Th\'{e}o},
  title =	{{The Rewster: Type Preserving Rewrite Rules for the Coq Proof Assistant}},
  booktitle =	{15th International Conference on Interactive Theorem Proving (ITP 2024)},
  pages =	{26:1--26:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-337-9},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{309},
  editor =	{Bertot, Yves and Kutsia, Temur and Norrish, Michael},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2024.26},
  URN =		{urn:nbn:de:0030-drops-207545},
  doi =		{10.4230/LIPIcs.ITP.2024.26},
  annote =	{Keywords: type theory, dependent types, rewrite rules, type preservation, Coq}
}
Document
DOI: 10.4230/OASIcs.FMBC.2024.7
Towards Formally Specifying and Verifying Smart Contract Upgrades in Coq

Authors: Derek Sorensen

Published in: OASIcs, Volume 118, 5th International Workshop on Formal Methods for Blockchains (FMBC 2024)

Abstract
Smart contract upgrades are costly from a verification perspective and can be a meaningful source of vulnerabilities when done incorrectly. Unfortunately, there is no established, formal framework through which one can reason about contracts as they undergo upgrades, though much work has been done to verify standalone smart contracts. Instead, one must repeat the full verification process for each contract upgrade, something which relies heavily on fallible intuition, can lead to unexpected vulnerabilities, and drives up the cost of formally verifying smart contracts. We propose a formal framework for contract upgrades in ConCert, a Coq-based smart contract verification tool. Central to this framework is our notion of a contract morphism, a theoretical tool which we introduce to formally encode structural relationships between smart contracts, and with which we can formally specify and verify an upgraded contract relative to its previous versions. We argue that ours is a natural framework for specifying and verifying contract upgrades, and hope to offer a first step towards rigorous, efficient specification and verification of contract upgrades.
Cite as

Derek Sorensen. Towards Formally Specifying and Verifying Smart Contract Upgrades in Coq. In 5th International Workshop on Formal Methods for Blockchains (FMBC 2024). Open Access Series in Informatics (OASIcs), Volume 118, pp. 7:1-7:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{sorensen:OASIcs.FMBC.2024.7,
  author =	{Sorensen, Derek},
  title =	{{Towards Formally Specifying and Verifying Smart Contract Upgrades in Coq}},
  booktitle =	{5th International Workshop on Formal Methods for Blockchains (FMBC 2024)},
  pages =	{7:1--7:14},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-317-1},
  ISSN =	{2190-6807},
  year =	{2024},
  volume =	{118},
  editor =	{Bernardo, Bruno and Marmsoler, Diego},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.FMBC.2024.7},
  URN =		{urn:nbn:de:0030-drops-198728},
  doi =		{10.4230/OASIcs.FMBC.2024.7},
  annote =	{Keywords: smart contract verification, formal methods, interactive theorem prover, smart contract upgrades}
}
Document
DOI: 10.4230/LIPIcs.ITP.2021.24
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.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
DOI: 10.4230/LIPIcs.ITP.2019.26
Ornaments for Proof Reuse in Coq

Authors: Talia Ringer, Nathaniel Yazdani, John Leo, and Dan Grossman

Published in: LIPIcs, Volume 141, 10th International Conference on Interactive Theorem Proving (ITP 2019)

Abstract
Ornaments express relations between inductive types with the same inductive structure. We implement fully automatic proof reuse for a particular class of ornaments in a Coq plugin, and show how such a tool can give programmers the rewards of using indexed inductive types while automating away many of the costs. The plugin works directly on Coq code; it is the first ornamentation tool for a non-embedded dependently typed language. It is also the first tool to automatically identify ornaments: To lift a function or proof, the user must provide only the source type, the destination type, and the source function or proof. In taking advantage of the mathematical properties of ornaments, our approach produces faster functions and smaller terms than a more general approach to proof reuse in Coq.
Cite as

Talia Ringer, Nathaniel Yazdani, John Leo, and Dan Grossman. Ornaments for Proof Reuse in Coq. In 10th International Conference on Interactive Theorem Proving (ITP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 141, pp. 26:1-26:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{ringer_et_al:LIPIcs.ITP.2019.26,
  author =	{Ringer, Talia and Yazdani, Nathaniel and Leo, John and Grossman, Dan},
  title =	{{Ornaments for Proof Reuse in Coq}},
  booktitle =	{10th International Conference on Interactive Theorem Proving (ITP 2019)},
  pages =	{26:1--26:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-122-1},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{141},
  editor =	{Harrison, John and O'Leary, John and Tolmach, Andrew},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2019.26},
  URN =		{urn:nbn:de:0030-drops-110816},
  doi =		{10.4230/LIPIcs.ITP.2019.26},
  annote =	{Keywords: ornaments, proof reuse, proof automation}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2019.25
Gluing for Type Theory

Authors: Ambrus Kaposi, Simon Huber, and Christian Sattler

Published in: LIPIcs, Volume 131, 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)

Abstract
The relationship between categorical gluing and proofs using the logical relation technique is folklore. In this paper we work out this relationship for Martin-Löf type theory and show that parametricity and canonicity arise as special cases of gluing. The input of gluing is two models of type theory and a pseudomorphism between them and the output is a displayed model over the first model. A pseudomorphism preserves the categorical structure strictly, the empty context and context extension up to isomorphism, and there are no conditions on preservation of type formers. We look at three examples of pseudomorphisms: the identity on the syntax, the interpretation into the set model and the global section functor. Gluing along these result in syntactic parametricity, semantic parametricity and canonicity, respectively.
Cite as

Ambrus Kaposi, Simon Huber, and Christian Sattler. Gluing for Type Theory. In 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 131, pp. 25:1-25:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{kaposi_et_al:LIPIcs.FSCD.2019.25,
  author =	{Kaposi, Ambrus and Huber, Simon and Sattler, Christian},
  title =	{{Gluing for Type Theory}},
  booktitle =	{4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)},
  pages =	{25:1--25: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.25},
  URN =		{urn:nbn:de:0030-drops-105323},
  doi =		{10.4230/LIPIcs.FSCD.2019.25},
  annote =	{Keywords: Martin-L\"{o}f type theory, logical relations, parametricity, canonicity, quotient inductive types}
}
Document
DOI: 10.4230/LIPIcs.TLCA.2015.226
Wild omega-Categories for the Homotopy Hypothesis in Type Theory

Authors: André Hirschowitz, Tom Hirschowitz, and Nicolas Tabareau

Published in: LIPIcs, Volume 38, 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015)

Abstract
In classical homotopy theory, the homotopy hypothesis asserts that the fundamental varpi-groupoid construction induces an equivalence between topological spaces and weak varpi-groupoids. In the light of Voevodsky's univalent foundations program, which puts forward an interpretation of types as topological spaces, we consider the question of transposing the homotopy hypothesis to type theory. Indeed such a transposition could stand as a new approach to specifying higher inductive types. Since the formalisation of general weak varpi-groupoids in type theory is a difficult task, we only take a first step towards this goal, which consists in exploring a shortcut through strict varpi-categories. The first outcome is a satisfactory type-theoretic notion of strict varpi-category, which has hsets of cells in all dimensions. For this notion, defining the 'fundamental strict varpi-category' of a type seems out of reach. The second outcome is an 'incoherently strict' notion of type-theoretic varpi-category, which admits arbitrary types of cells in all dimensions. These are the 'wild' varpi-categories of the title. They allow the definition of a 'fundamental wild varpi-category' map, which leads to our (partial) homotopy hypothesis for type theory (stating an adjunction, not an equivalence). All of our results have been formalised in the Coq proof assistant. Our formalisation makes systematic use of the machinery of coinductive types.
Cite as

André Hirschowitz, Tom Hirschowitz, and Nicolas Tabareau. Wild omega-Categories for the Homotopy Hypothesis in Type Theory. In 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 38, pp. 226-240, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{hirschowitz_et_al:LIPIcs.TLCA.2015.226,
  author =	{Hirschowitz, Andr\'{e} and Hirschowitz, Tom and Tabareau, Nicolas},
  title =	{{Wild omega-Categories for the Homotopy Hypothesis in Type Theory}},
  booktitle =	{13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015)},
  pages =	{226--240},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-87-3},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{38},
  editor =	{Altenkirch, Thorsten},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TLCA.2015.226},
  URN =		{urn:nbn:de:0030-drops-51669},
  doi =		{10.4230/LIPIcs.TLCA.2015.226},
  annote =	{Keywords: Homotopy Type theory; Omega-categories; Coinduction; Homotopy hypothesis}
}
  • Refine by Author
  • 2 Tabareau, Nicolas
  • 1 Gilbert, Gaëtan
  • 1 Grossman, Dan
  • 1 Hirschowitz, André
  • 1 Hirschowitz, Tom
  • Show More...

  • Refine by Classification

  • Refine by Keyword
  • 2 Coq
  • 1 Bidirectional Typing
  • 1 Calculus of Inductive Constructions
  • 1 Homotopy Type theory; Omega-categories; Coinduction; Homotopy hypothesis
  • 1 Martin-Löf type theory
  • Show More...

  • Refine by Type
  • 6 document

  • Refine by Publication Year
  • 2 2019
  • 2 2024
  • 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
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact