The computability path ordering

Autor: Frédéric Blanqui, Jean-Pierre Jouannaud, Albert Rubio

Publikováno v: Logical Methods in Computer Science, Vol Volume 11, Issue 4 (2015)

This paper aims at carrying out termination proofs for simply typed higher-order calculi automatically by using ordering comparisons. To this end, we introduce the computability path ordering (CPO), a recursive relation on terms obtained by lifting a

Externí odkaz: https://doaj.org/article/3dbfe0beeec54bfe8b0628680baeee71

Confluence in Non-Left-Linear Untyped Higher-Order Rewrite Theories

Autor: Jean-Pierre Jouannaud, Gaspard Férey

Publikováno v: PPDP 2021-23rd International Symposium on Principles and Practice of Declarative Programming
PPDP 2021-23rd International Symposium on Principles and Practice of Declarative Programming, Sep 2021, Tallin, Estonia. ⟨10.1145/NNNNNNN.NNNNNNN⟩
PPDP
PPDP 2021-23rd International Symposium on Principles and Practice of Declarative Programming, Sep 2021, Tallin, Estonia. ⟨10.1145/3479394.3479403⟩

International audience; We develop techniques based on van Oostrom's decreasing diagrams that reduce confluence proofs to the checking of critical pairs for higher-order rewrite rules extending betareduction on pure lambda-terms. We show that conflue

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::ddf7ecfd90f8b32955d498cc643a88a0
https://hal.inria.fr/hal-03126115

Corrigendum to 'Inductive-data-type systems' [Theoret. Comput. Sci. 272 (1–2) (2002) 41–68]

Autor: Frédéric Blanqui, Mitsuhiro Okada, Jean Pierre Jouannaud

Publikováno v: Theoretical Computer Science. 817:81-82

In a previous work (Abstract data type systems, Theoret. Comput. Sci. 173 (2) (1997)), the last two authors presented a combined language made of a (strongly normalizing) algebraic rewrite system and a typed lambda-calculus enriched by pattern-matchi

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_________::f69a0b97b281b6157c722193b3fc6f61
https://doi.org/10.1016/j.tcs.2018.01.010

Coq without Type Casts: A Complete Proof of Coq Modulo Theory

Autor: Jean-Pierre Jouannaud, Pierre-Yves Strub

Publikováno v: LPAR-21: 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning
LPAR-21: 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning, May 2017, Maun, Botswana
LPAR

Incorporating extensional equality into a dependent intensional type system such as the Calculus of Constructions provides with stronger type-checking capabilities and makes the proof development closer to intuition. Since strong forms of extensional

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::f6a491f30fbfd0e605c04d9102df29d4
https://inria.hal.science/hal-01664457/document

Polymorphic higher-order recursive path orderings

Autor: Jean-Pierre Jouannaud, Albert Rubio

Publikováno v: Journal of the ACM. 54:1-48

This article extends the termination proof techniques based on reduction orderings to a higher-order setting, by defining a family of recursive path orderings for terms of a typed lambda-calculus generated by a signature of polymorphic higher-order f

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_________::5f3f4a0082d843f55bd4469b947ff606
https://doi.org/10.1145/1206035.1206037