Result: Pure patterns Type systems

Title:
Pure patterns Type systems
Authors:
BARTHE, Gilles, CIRSTEA, Horatiu, KIRCHNER, Claude, LIQUORI, Luigi
Source:
Conference record of POPL® 2003: the 30th ACM SIGPLAN-SIGACT symposium on principles of programming languages®, New Orleans, Louisiana, USA, January 15-17, 2003ACM SIGPLAN notices. 38(1):250-261
Publisher Information:
Broadway, NY: ACM, 2003.
Publication Year:
2003
Physical Description:
print, 30 ref
Original Material:
INIST-CNRS
Subject Terms:
Computer science, Informatique, Sciences exactes et technologie, Exact sciences and technology, Sciences appliquees, Applied sciences, Informatique; automatique theorique; systemes, Computer science; control theory; systems, Informatique théorique, Theoretical computing, Théorie des langages et analyse syntaxique, Language theory and syntactical analysis, Algorithmique. Calculabilité. Arithmétique ordinateur, Algorithmics. Computability. Computer arithmetics, Concordance forme, Pattern matching, Isomorphisme, Isomorphism, Isomorfismo, Lambda calcul, Lambda calculus, Lambda cálculo, Langage programmation, Programming language, Lenguaje programación, Logique formelle, Formal logic, Lógica formal, Programmation logique avec contrainte, Constraint logic programming, Programación lógica con restricción, Réécriture, Rewriting, Reescritura, Système algébrique, Algebraic system
Document Type:
Conference Conference Paper
File Description:
text
Language:
English
Author Affiliations:
INRIA, BP 93, 06902 Sophia Antipolis, France
LORIA, INRIA & University Nancy II, BP 239, 54506 Vandoeuvre-lès-Nancy, United States
ISSN:
1523-2867
Access URL:
http://pascal-francis.inist.fr/vibad/index.php?action=search&terms=14651511
Rights:
Copyright 2003 INIST-CNRS
CC BY 4.0
Sauf mention contraire ci-dessus, le contenu de cette notice bibliographique peut être utilisé dans le cadre d’une licence CC BY 4.0 Inist-CNRS / Unless otherwise stated above, the content of this bibliographic record may be used under a CC BY 4.0 licence by Inist-CNRS / A menos que se haya señalado antes, el contenido de este registro bibliográfico puede ser utilizado al amparo de una licencia CC BY 4.0 Inist-CNRS
Notes:
Computer science; theoretical automation; systems
Accession Number:
edscal.14651511
Database:
PASCAL Archive

Further Information

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 settling 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.