3 Search Results for "Hermant, Olivier"

Document
DOI: 10.4230/LIPIcs.FSCD.2020.31
Encoding Agda Programs Using Rewriting

Authors: Guillaume Genestier

Published in: LIPIcs, Volume 167, 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)

Abstract
We present in this paper an encoding in an extension with rewriting of the Edimburgh Logical Framework (LF) [Harper et al., 1993] of two common features: universe polymorphism and eta-convertibility. This encoding is at the root of the translator between Agda and Dedukti developped by the author.
Cite as

Guillaume Genestier. Encoding Agda Programs Using Rewriting. In 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 167, pp. 31:1-31:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{genestier:LIPIcs.FSCD.2020.31,
  author =	{Genestier, Guillaume},
  title =	{{Encoding Agda Programs Using Rewriting}},
  booktitle =	{5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)},
  pages =	{31:1--31:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-155-9},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{167},
  editor =	{Ariola, Zena M.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2020.31},
  URN =		{urn:nbn:de:0030-drops-123530},
  doi =		{10.4230/LIPIcs.FSCD.2020.31},
  annote =	{Keywords: Logical Frameworks, Rewriting, Universe Polymorphism, Eta Conversion}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2019.9
Dependency Pairs Termination in Dependent Type Theory Modulo Rewriting

Authors: Frédéric Blanqui, Guillaume Genestier, and Olivier Hermant

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

Abstract
Dependency pairs are a key concept at the core of modern automated termination provers for first-order term rewriting systems. In this paper, we introduce an extension of this technique for a large class of dependently-typed higher-order rewriting systems. This extends previous results by Wahlstedt on the one hand and the first author on the other hand to strong normalization and non-orthogonal rewriting systems. This new criterion is implemented in the type-checker Dedukti.
Cite as

Frédéric Blanqui, Guillaume Genestier, and Olivier Hermant. Dependency Pairs Termination in Dependent Type Theory Modulo Rewriting. In 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 131, pp. 9:1-9:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{blanqui_et_al:LIPIcs.FSCD.2019.9,
  author =	{Blanqui, Fr\'{e}d\'{e}ric and Genestier, Guillaume and Hermant, Olivier},
  title =	{{Dependency Pairs Termination in Dependent Type Theory Modulo Rewriting}},
  booktitle =	{4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)},
  pages =	{9:1--9:21},
  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.9},
  URN =		{urn:nbn:de:0030-drops-105167},
  doi =		{10.4230/LIPIcs.FSCD.2019.9},
  annote =	{Keywords: termination, higher-order rewriting, dependent types, dependency pairs}
}
Document
DOI: 10.4230/LIPIcs.RTA.2012.133
A Semantic Proof that Reducibility Candidates entail Cut Elimination

Authors: Denis Cousineau and Olivier Hermant

Published in: LIPIcs, Volume 15, 23rd International Conference on Rewriting Techniques and Applications (RTA'12) (2012)

Abstract
Two main lines have been adopted to prove the cut elimination theorem: the syntactic one, that studies the process of reducing cuts, and the semantic one, that consists in interpreting a sequent in some algebra and extracting from this interpretation a cut-free proof of this very sequent. A link between those two methods was exhibited by studying in a semantic way, syntactical tools that allow to prove (strong) normalization of proof-terms, namely reducibility candidates. In the case of deduction modulo, a framework combining deduction and rewriting rules in which theories like Zermelo set theory and higher order logic can be expressed, this is obtained by constructing a reducibility candidates valued model. The existence of such a pre-model for a theory entails strong normalization of its proof-terms and, by the usual syntactic argument, the cut elimination property. In this paper, we strengthen this gate between syntactic and semantic methods, by providing a full semantic proof that the existence of a pre-model entails the cut elimination property for the considered theory in deduction modulo. We first define a new simplified variant of reducibility candidates à la Girard, that is sufficient to prove weak normalization of proof-terms (and therefore the cut elimination property). Then we build, from some model valued on the pre-Heyting algebra of those WN reducibility candidates, a regular model valued on a Heyting algebra on which we apply the usual soundness/strong completeness argument. Finally, we discuss further extensions of this new method towards normalization by evaluation techniques that commonly use Kripke semantics.
Cite as

Denis Cousineau and Olivier Hermant. A Semantic Proof that Reducibility Candidates entail Cut Elimination. In 23rd International Conference on Rewriting Techniques and Applications (RTA'12). Leibniz International Proceedings in Informatics (LIPIcs), Volume 15, pp. 133-148, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)

Copy BibTex To Clipboard

@InProceedings{cousineau_et_al:LIPIcs.RTA.2012.133,
  author =	{Cousineau, Denis and Hermant, Olivier},
  title =	{{A Semantic Proof that Reducibility Candidates entail Cut Elimination}},
  booktitle =	{23rd International Conference on Rewriting Techniques and Applications (RTA'12)},
  pages =	{133--148},
  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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2012.133},
  URN =		{urn:nbn:de:0030-drops-34899},
  doi =		{10.4230/LIPIcs.RTA.2012.133},
  annote =	{Keywords: cut elimination, reducibility candidates, (pre-)Heyting algebras}
}
  • Refine by Author
  • 2 Genestier, Guillaume
  • 2 Hermant, Olivier
  • 1 Blanqui, Frédéric
  • 1 Cousineau, Denis

  • Refine by Classification
  • 2 Theory of computation → Equational logic and rewriting
  • 2 Theory of computation → Type theory

  • Refine by Keyword
  • 1 (pre-)Heyting algebras
  • 1 Eta Conversion
  • 1 Logical Frameworks
  • 1 Rewriting
  • 1 Universe Polymorphism
  • Show More...

  • Refine by Type
  • 3 document

  • Refine by Publication Year
  • 1 2012
  • 1 2019
  • 1 2020

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 Imprint Privacy Contact