Pure Patterns Type Systems

Gilles Barthe (1) , Horatiu Cirstea (2) , Claude Kirchner (2) , Luigi Liquori (3, 4)

1 LEMME - Software and mathematics
2 PROTHEO - Constraints, automatic deduction and software properties proofs
3 LOGNET - Logical Networks: Self-organizing Overlay Networks and Programmable Overlay Computing Systems
4 MIRHO - Objects, types and prototypes : semantics and validation

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 classical (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.

Mots clés: rewriting; lambda calculus; pure type systems

Mots clés: matching; réécriture; lambda calcul; pure type systèmes; filtrage

Domaines: Informatique et langage [cs.CL]; Logique en informatique [cs.LO]

Gilles Barthe, Horatiu Cirstea, Claude Kirchner, Luigi Liquori. Pure Patterns Type Systems. Proceedings of the 30th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL, New Orleans, LA, USA — January 15 - 17, 2003, Jan 2003, New Orleans, United States. pp.250 - 261, ⟨10.1145/604131.604152⟩. ⟨inria-00099463v2⟩