Type theory and rewriting
Logic in Computer Science
2016-08-16 v2
Authors:
Frédéric Blanqui
Abstract
We study the properties, in particular termination, of dependent types systems for lambda calculus and rewriting.
Keywords
Cite
@article{arxiv.cs/0610068,
title = {Type theory and rewriting},
author = {Frédéric Blanqui},
journal= {arXiv preprint arXiv:cs/0610068},
year = {2016}
}
Comments
English version of my PhD thesis
Related papers
View all related →
Logic in Computer Science · Computer Science
A type-based termination criterion for dependently-typed higher-order rewrite systems
Frederic Blanqui
2007-05-23
Logic in Computer Science · Computer Science
A Note on Confluence in Typed Probabilistic Lambda Calculi
Rafael Romero, Alejandro Díaz-Caro
2022-04-11
Logic in Computer Science · Computer Science
Dependency Pairs Termination in Dependent Type Theory Modulo Rewriting
Frédéric Blanqui, Guillaume Genestier, Olivier Hermant
2020-07-16
Logic in Computer Science · Computer Science
Probabilistic Rewriting and Asymptotic Behaviour: on Termination and Unique Normal Forms
Claudia Faggian
2023-06-22
Logic in Computer Science · Computer Science
Type safety of rewrite rules in dependent types
Frédéric Blanqui
2020-11-02
Logic in Computer Science · Computer Science
Termination of $\lambda$$\Pi$ modulo rewriting using the size-change principle (work in progress)
Frédéric Blanqui, Guillaume Genestier
2018-12-06
Logic in Computer Science · Computer Science
Decidability of Type-checking in the Calculus of Algebraic Constructions with Size Annotations
Frédéric Blanqui
2016-08-16
Logic in Computer Science · Computer Science
The Vectorial $\lambda$-Calculus
Pablo Arrighi, Alejandro Díaz-Caro, Benoît Valiron
2017-05-12
Logic in Computer Science · Computer Science
Rewriting modulo in Deduction modulo
Frédéric Blanqui
2016-08-16
Logic in Computer Science · Computer Science
Linearization via Rewriting (Long Version)
Ugo Dal Lago, Federico Olimpieri
2025-03-26
Logic · Mathematics
Dependent dreams: recounting types
Saharon Shelah
2012-02-28
Logic in Computer Science · Computer Science
Combining typing and size constraints for checking the termination of higher-order conditional rewrite systems
Frédéric Blanqui, Colin Riba
2016-08-16
Programming Languages · Computer Science
A Rewriting View of Simple Typing
Aaron Stump, Garrin Kimmell, Hans Zantema, Ruba El Haj Omar
2015-07-01
Logic in Computer Science · Computer Science
A Type System for the Vectorial Aspect of the Linear-Algebraic Lambda-Calculus
Pablo Arrighi, Alejandro Díaz-Caro, Benoît Valiron
2012-08-01
Logic in Computer Science · Computer Science
Refinement Types as Higher Order Dependency Pairs
Cody Roux
2011-01-25
Logic in Computer Science · Computer Science
Number representations and term rewriting
Boas Kluiving, Wijnand van Woerkom
2016-07-18
Symbolic Computation · Computer Science
On Probabilistic Term Rewriting
Martin Avanzini, Ugo Dal Lago, Akihisa Yamada
2018-02-28
Logic in Computer Science · Computer Science
Lambda Calculus with Explicit Read-back
Anton Salikhmetov
2018-08-21
Logic in Computer Science · Computer Science
Size-based termination of higher-order rewriting
Frédéric Blanqui
2018-02-21
Logic in Computer Science · Computer Science
Typed lambda-terms in categorical attributed graph transformation
Bertrand Boisvert, Louis Féraud, Sergei Soloviev
2011-07-04
Logic in Computer Science · Computer Science
Termination of rewrite relations on $\lambda$-terms based on Girard's notion of reducibility
Frédéric Blanqui
2015-09-03
Logic in Computer Science · Computer Science
An Investigation of Kripke-style Modal Type Theories
Jason Z. S. Hu, Brigitte Pientka
2023-05-12
Logic in Computer Science · Computer Science
A Type System for Required/Excluded Elements in CLS
Mariangiola Dezani-Ciancaglini, Paola Giannini, Angelo Troina
2009-11-13
Logic in Computer Science · Computer Science
Dependent choice as a termination principle
Thomas Powell
2019-02-28
Logic in Computer Science · Computer Science
Foundations of Substructural Dependent Type Theory
C. B. Aberlé
2024-01-30