Type theory and rewriting

2006/10/11 by Frédéric Blanqui, Blanqui, Frédéric
Computer Science · #FOS: Computer and information sciences #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Logic, Reasoning, and Knowledge #Logic, programming, and type systems #cs.LO

paper · pdf · doi:10.48550/arxiv.cs/0610068

English version of my PhD thesis

openalex publication_date 2006/10/11 · arxiv created 2007/02/22 · arxiv updated 2016/08/16 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28

Abstract

We study the properties, in particular termination, of dependent types systems for lambda calculus and rewriting.

Related

• The Formal System lambda-delta
• An extended type system with lambda-typed lambda-expressions (extended version)
• On the Formal Metatheory of the Pure Type Systems using One-sorted Variable Names and Multiple Substitutions
• An overview of type theories
• Linearization via Rewriting (Long Version)