2 Search Results for "Barras, Bruno"

Document
System Description
DOI: 10.4230/LIPIcs.FSCD.2020.35
The New Rewriting Engine of Dedukti (System Description)

Authors: Gabriel Hondet and Frédéric Blanqui

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

Abstract
Dedukti is a type-checker for the λΠ-calculus modulo rewriting, an extension of Edinburgh’s logical framework LF where functions and type symbols can be defined by rewrite rules. It therefore contains an engine for rewriting LF terms and types according to the rewrite rules given by the user. A key component of this engine is the matching algorithm to find which rules can be fired. In this paper, we describe the class of rewrite rules supported by Dedukti and the new implementation of the matching algorithm. Dedukti supports non-linear rewrite rules on terms with binders using higher-order pattern-matching as in Combinatory Reduction Systems (CRS). The new matching algorithm extends the technique of decision trees introduced by Luc Maranget in the OCaml compiler to this more general context.
Cite as

Gabriel Hondet and Frédéric Blanqui. The New Rewriting Engine of Dedukti (System Description). In 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 167, pp. 35:1-35:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{hondet_et_al:LIPIcs.FSCD.2020.35,
  author =	{Hondet, Gabriel and Blanqui, Fr\'{e}d\'{e}ric},
  title =	{{The New Rewriting Engine of Dedukti}},
  booktitle =	{5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)},
  pages =	{35:1--35:16},
  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.35},
  URN =		{urn:nbn:de:0030-drops-123577},
  doi =		{10.4230/LIPIcs.FSCD.2020.35},
  annote =	{Keywords: rewriting, higher-order pattern-matching, decision trees}
}
Document
DOI: 10.4230/LIPIcs.CSL.2013.653
Semantics of Intensional Type Theory extended with Decidable Equational Theories

Authors: Qian Wang and Bruno Barras

Published in: LIPIcs, Volume 23, Computer Science Logic 2013 (CSL 2013)

Abstract
Incorporating extensional equality into a dependent intensional type system such as the Calculus of Constructions (CC) provides with stronger type-checking capabilities and makes the proof development closer to intuition. Since strong forms of extensionality generally leads to undecidable type-checking, it seems a reasonable trade-off to extend intensional equality with a decidable first-order theory, as experimented in earlier work on CoqMTU and its implementation CoqMT. In this work, CoqMTU is extended with strong eliminations. The meta-theoretical study, particularly the part relying on semantic arguments, is more complex. A set-theoretical model of the equational theory is the key ingredient to derive the logical consistency of the formalism. Strong normalization, the main lemma from which type-decidability follows, is proved by attaching realizability information to the values of the model. The approach we have followed is to first consider an abstract notion of first-order equational theory, and then instantiate it with a particular instance, Presburger Arithmetic. These results have been formalized using Coq.
Cite as

Qian Wang and Bruno Barras. Semantics of Intensional Type Theory extended with Decidable Equational Theories. In Computer Science Logic 2013 (CSL 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 23, pp. 653-667, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)

Copy BibTex To Clipboard

@InProceedings{wang_et_al:LIPIcs.CSL.2013.653,
  author =	{Wang, Qian and Barras, Bruno},
  title =	{{Semantics of Intensional Type Theory extended with Decidable Equational Theories}},
  booktitle =	{Computer Science Logic 2013 (CSL 2013)},
  pages =	{653--667},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-60-6},
  ISSN =	{1868-8969},
  year =	{2013},
  volume =	{23},
  editor =	{Ronchi Della Rocca, Simona},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2013.653},
  URN =		{urn:nbn:de:0030-drops-42241},
  doi =		{10.4230/LIPIcs.CSL.2013.653},
  annote =	{Keywords: Calculus of Constructions, Extensional Type Theory, Intensional Type Theory, Model, Meta-theory, Consistency, Strong Normalization, Presburger Arithme}
}
  • Refine by Author
  • 1 Barras, Bruno
  • 1 Blanqui, Frédéric
  • 1 Hondet, Gabriel
  • 1 Wang, Qian

  • Refine by Classification
  • 1 Theory of computation → Equational logic and rewriting
  • 1 Theory of computation → Operational semantics

  • Refine by Keyword
  • 1 Calculus of Constructions
  • 1 Consistency
  • 1 Extensional Type Theory
  • 1 Intensional Type Theory
  • 1 Meta-theory
  • Show More...

  • Refine by Type
  • 2 document

  • Refine by Publication Year
  • 1 2013
  • 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