Pure Patterns Type Systems

Gilles Barthe 1 Horatiu Cirstea 2 Claude Kirchner 2 Luigi Liquori 3, 4
1 LEMME - Software and mathematics
CRISAM - Inria Sophia Antipolis - Méditerranée
2 PROTHEO - Constraints, automatic deduction and software properties proofs
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
4 MIRHO - Objects, types and prototypes : semantics and validation
CRISAM - Inria Sophia Antipolis - Méditerranée , UHP - Université Henri Poincaré - Nancy 1, Université Nancy 2, INPL - Institut National Polytechnique de Lorraine, CNRS - Centre National de la Recherche Scientifique : UMR7503
Abstract : 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.
Type de document :
Communication dans un congrès
ACM. 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, 2003, 〈10.1145/604131.604152〉
Liste complète des métadonnées

Littérature citée [30 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00099463
Contributeur : Luigi Liquori <>
Soumis le : mercredi 13 mai 2015 - 12:09:08
Dernière modification le : samedi 27 janvier 2018 - 01:31:34
Document(s) archivé(s) le : mercredi 19 avril 2017 - 19:34:04

Fichier

2003-popl-03.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Gilles Barthe, Horatiu Cirstea, Claude Kirchner, Luigi Liquori. Pure Patterns Type Systems. ACM. 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, 2003, 〈10.1145/604131.604152〉. 〈inria-00099463v2〉

Partager

Métriques

Consultations de la notice

454

Téléchargements de fichiers

70