Reductions in Higher-Order Rewriting and Their Equivalence

Autor: Barenbaum, Pablo, Bonelli, Eduardo

Proof terms are syntactic expressions that represent computations in term rewriting. They were introduced by Meseguer and exploited by van Oostrom and de Vrijer to study equivalence of reductions in (left-linear) first-order term rewriting systems. W

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::ea85a5e9b702ee33cdf6c979413dbcb8

Size-Based Termination for Non-Positive Types in Simply Typed Lambda-Calculus

Autor: Takahashi, Yuta

So far, several typed lambda-calculus systems were combined with algebraic rewrite rules, and the termination (in other words, strong normalisation) problem of the combined systems was discussed. By the size-based approach, Blanqui formulated a termi

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_________::5f6d4737cd5c551ebdbb2df9a0da8175

Type Theory Unchained: Extending Agda with User-Defined Rewrite Rules

Autor: Cockx, J.G.H., Bezem, Marc, Mahboubi, Assia

Publikováno v: 25th International Conference on Types for Proofs and Programs, TYPES 2019

Dependently typed languages such as Coq and Agda can statically guarantee the correctness of our proofs and programs. To provide this guarantee, they restrict users to certain schemes a- such as strictly positive datatypes, complete case analysis, an

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::654ee643df892f152b9ac7c03720f496
http://resolver.tudelft.nl/uuid:4a736a78-dba3-4afe-baea-4c4bac9b515c

Dependency Pairs Termination in Dependent Type Theory Modulo Rewriting

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

Publikováno v: FSCD 2019-4th International Conference on Formal Structures for Computation and Deduction
FSCD 2019-4th International Conference on Formal Structures for Computation and Deduction, Jun 2019, Dortmund, Germany. ⟨10.4230/LIPIcs.FSCD.2019.9⟩
TYPES 2019-25th International Conference on Types for Proofs and Programs
TYPES 2019-25th International Conference on Types for Proofs and Programs, Jun 2019, Oslo, Norway. pp.30-31
HAL

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 sy

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::20e987b76c26da217afa272fd0eef820
https://hal.inria.fr/hal-01943941v4/document

Quelques ponts entre sémantique opérationnelle et modèles dénotationnels des langages de programmation

Autor: Tom Hirschowitz

Publikováno v: Logique en informatique [cs.LO]. Université Grenoble Alpes, 2016
HAL

Le fil directeur de ce manuscrit réside dans la volonté demathématiser l'activité des chercheurs en programmation. Exactementcomme la définition de groupe a émergé d'une quantité suffisante decas particuliers, on y tente d'abstraire et de gé

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=dedup_wf_001::7fba41b1aa0cfbb2c46fac8d185c0ddd
https://hal.archives-ouvertes.fr/tel-01400666/file/hdr.pdf