Termination of $\lambda$$\Pi$ modulo rewriting using the size-change principle (work in progress)

Autor: Blanqui, Frédéric, Genestier, Guillaume

Publikováno v: 16th International Workshop on Termination, Jul 2018, Oxford, United Kingdom

The Size-Change Termination principle was first introduced to study the termination of first-order functional programs. In this work, we show that it can also be used to study the termination of higher-order rewriting in a system of dependent types e

Externí odkaz: http://arxiv.org/abs/1812.01853

Encoding Agda Programs Using Rewriting

Autor: Genestier, Guillaume

Publikováno v: FSCD-5th International Conference on Formal Structures for Computation and Deduction
FSCD-5th International Conference on Formal Structures for Computation and Deduction, Jun 2020, Paris, France. ⟨10.4230/LIPIcs.FSCD.2020.31⟩

International audience; 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 ro

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

Termination of λΠ modulo rewriting using the size-change principle (work in progress)

Autor: Blanqui, Frédéric, Genestier, Guillaume

Publikováno v: 16th International Workshop on Termination
16th International Workshop on Termination, Jul 2018, Oxford, United Kingdom. pp. 10-14

International audience; The Size-Change Termination principle was first introduced to study the termination of first-order functional programs. In this work, we show that it can also be used to study the termination of higher-order rewriting in a sys

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=dedup_wf_001::2da5719317121f7dd316a1aefca90b0f
https://hal.inria.fr/hal-01944731/file/main.pdf

Termination checking in the λΠ-calculus modulo theory.From a practical and a theoretical viewpoint

Autor: Genestier, Guillaume

Publikováno v: Logic in Computer Science [cs.LO]. 2017

National audience; Dedukti is a type-checker for the λΠ-calculus modulo theory, which has theparticularity to allow the user to declare rewrite rules, especially in order toencode the logic he/she wants to use. Thanks to the Curry-Howard-De Bruijnc

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=dedup_wf_001::50840db7b3c8c602f6533805c3a2cd28
https://inria.hal.science/hal-01676409/file/Genestier_RapportLMFI.pdf