Pure patterns type systems

9 years 10 months ago
Pure patterns type systems
We introduce a new framework of algebraic pure type systems in which we consider rewrite rules as lambda terms with patterns and rewrite rule application as abstraction application with built-in matching facilities. This framework, that we call "Pure Pattern Type Systems", is particularly well-suited for the foundations of programming (meta)languages and proof assistants since it provides in a fully unified setting higher-order capabilities and pattern matching ability together with powerful type systems. We prove some standard properties like confluence and subject reduction for the case of a syntactic theory and under a syntactical restriction over the shape of patterns. We also conjecture the strong normalization of typable terms. This work should be seen as a contribution to a formal connection between logics and rewriting, and a step towards new proof engines based on the Curry-Howard isomorphism. Categories and Subject Descriptors D.3.1 [Formal Definitions and Theory]:...
Gilles Barthe, Horatiu Cirstea, Claude Kirchner, L
Added 03 Dec 2009
Updated 03 Dec 2009
Type Conference
Year 2003
Where POPL
Authors Gilles Barthe, Horatiu Cirstea, Claude Kirchner, Luigi Liquori
Comments (0)