Pure Patterns Type Systems
Identifieur interne : 007820 ( Main/Merge ); précédent : 007819; suivant : 007821Pure Patterns Type Systems
Auteurs : Gilles Barthe ; Horatiu Cirstea ; Claude Kirchner ; Luigi LiquoriSource :
English descriptors
- KwdEn :
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.
Links toward previous steps (curation, corpus...)
- to stream Crin, to step Corpus: 003738
- to stream Crin, to step Curation: 003738
- to stream Crin, to step Checkpoint: 000984
Links to Exploration step
CRIN:barthe03aLe document en format XML
<record><TEI><teiHeader><fileDesc><titleStmt><title xml:lang="fr" wicri:score="-121">Pure Patterns Type Systems</title></titleStmt><publicationStmt><idno type="RBID">CRIN:barthe03a</idno><date when="2003" year="2003">2003</date><idno type="wicri:Area/Crin/Corpus">003738</idno><idno type="wicri:Area/Crin/Curation">003738</idno><idno type="wicri:explorRef" wicri:stream="Crin" wicri:step="Curation">003738</idno><idno type="wicri:Area/Crin/Checkpoint">000984</idno><idno type="wicri:explorRef" wicri:stream="Crin" wicri:step="Checkpoint">000984</idno><idno type="wicri:Area/Main/Merge">007820</idno></publicationStmt><sourceDesc><biblStruct><analytic><title xml:lang="fr">Pure Patterns Type Systems</title><author><name sortKey="Barthe, Gilles" sort="Barthe, Gilles" uniqKey="Barthe G" first="Gilles" last="Barthe">Gilles Barthe</name></author><author><name sortKey="Cirstea, Horatiu" sort="Cirstea, Horatiu" uniqKey="Cirstea H" first="Horatiu" last="Cirstea">Horatiu Cirstea</name></author><author><name sortKey="Kirchner, Claude" sort="Kirchner, Claude" uniqKey="Kirchner C" first="Claude" last="Kirchner">Claude Kirchner</name></author><author><name sortKey="Liquori, Luigi" sort="Liquori, Luigi" uniqKey="Liquori L" first="Luigi" last="Liquori">Luigi Liquori</name></author></analytic></biblStruct></sourceDesc></fileDesc><profileDesc><textClass><keywords scheme="KwdEn" xml:lang="en"><term>lambda calculus</term><term>matching</term><term>pure type systems</term><term>rewriting</term></keywords></textClass></profileDesc></teiHeader><front><div type="abstract" xml:lang="en" wicri:score="2666">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.</div></front></TEI></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Main/Merge
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 007820 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Main/Merge/biblio.hfd -nk 007820 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= Main
|étape= Merge
|type= RBID
|clé= CRIN:barthe03a
|texte= Pure Patterns Type Systems
}}
| This area was generated with Dilib version V0.6.33. |  |