Decidability of type-checking in the calculus of algebraic constructions with size annotations
Identifieur interne :
000519 ( PascalFrancis/Corpus );
précédent :
000518;
suivant :
000520
Decidability of type-checking in the calculus of algebraic constructions with size annotations
Auteurs : Frédéric BlanquiSource :
-
Lecture notes in computer science [ 0302-9743 ] ; 2005.
RBID : Pascal:05-0409388
Descripteurs français
- Pascal (Inist)
- Programmation logique,
Décidabilité,
Théorie type,
Démonstration automatique,
Vérification programme,
Automatisation,
Langage ML,
Induction,
Annotation,
Réécriture,
Rho calcul,
Modélisation,
Problème terminaison,
..
English descriptors
- KwdEn :
- Annotation,
Automatic proving,
Automation,
Decidability,
Induction,
Logical programming,
ML language,
Modeling,
Program verification,
Rewriting,
Rho calculus,
Termination problem,
Type theory.
Abstract
Since Val Tannen's pioneering work on the combination of simply-typed A-calculus and first-order rewriting [11], many authors have contributed to this subject by extending it to richer typed A-calculi and rewriting paradigms, culminating in the Calculus of Algebraic Constructions. These works provide theoretical foundations for type-theoretic proof assistants where functions and predicates are defined by oriented higher-order equations. This kind of definitions subsumes usual inductive definitions, is easier to write and provides more automation. On the other hand, checking that such user-defined rewrite rules, when combined with β-reduction, are strongly normalizing and confluent, and preserve the decidability of type-checking, is more difficult. Most termination criteria rely on the term structure. In a previous work, we extended to dependent types and higher-order rewriting, the notion of "sized types" studied by several authors in the simpler framework of ML-like languages, and proved that it preserves strong normalization. The main contribution of the present paper is twofold. First, we prove that, in the Calculus of Algebraic Constructions with size annotations, the problems of type inference and type-checking are decidable, provided that the sets of constraints generated by size annotations are satisfiable and admit most general solutions. Second, we prove the latter properties for a size algebra rich enough for capturing usual induction-based definitions and much more.
Notice en format standard (ISO 2709)
Pour connaître la documentation sur le format Inist Standard.
| pA |
| A01 | 01 | 1 | | @0 0302-9743 |
|---|
| A05 | | | | @2 3634 |
|---|
| A08 | 01 | 1 | ENG | @1 Decidability of type-checking in the calculus of algebraic constructions with size annotations |
|---|
| A09 | 01 | 1 | ENG | @1 CSL 2005 : computer science logic : Oxford, 22-25 August 2005 |
|---|
| A11 | 01 | 1 | | @1 BLANQUI (Frédéric) |
|---|
| A12 | 01 | 1 | | @1 ONG (Luke) @9 ed. |
|---|
| A14 | 01 | | | @1 Laboratoire Lorrain de Recherche en Informatique et Automatique (LORIA) Institut National de Recherche en Informatique et Automatique (INRIA) 615 rue du Jardin Botanique, BP 101 @2 54602 Villers-lès-Nancy @3 FRA @Z 1 aut. |
|---|
| A20 | | | | @1 135-150 |
|---|
| A21 | | | | @1 2005 |
|---|
| A23 | 01 | | | @0 ENG |
|---|
| A26 | 01 | | | @0 3-540-28231-9 |
|---|
| A43 | 01 | | | @1 INIST @2 16343 @5 354000124413180110 |
|---|
| A44 | | | | @0 0000 @1 © 2005 INIST-CNRS. All rights reserved. |
|---|
| A45 | | | | @0 30 ref. |
|---|
| A47 | 01 | 1 | | @0 05-0409388 |
|---|
| A60 | | | | @1 P @2 C |
|---|
| A61 | | | | @0 A |
|---|
| A64 | 01 | 1 | | @0 Lecture notes in computer science |
|---|
| A66 | 01 | | | @0 DEU |
|---|
| C01 | 01 | | ENG | @0 Since Val Tannen's pioneering work on the combination of simply-typed A-calculus and first-order rewriting [11], many authors have contributed to this subject by extending it to richer typed A-calculi and rewriting paradigms, culminating in the Calculus of Algebraic Constructions. These works provide theoretical foundations for type-theoretic proof assistants where functions and predicates are defined by oriented higher-order equations. This kind of definitions subsumes usual inductive definitions, is easier to write and provides more automation. On the other hand, checking that such user-defined rewrite rules, when combined with β-reduction, are strongly normalizing and confluent, and preserve the decidability of type-checking, is more difficult. Most termination criteria rely on the term structure. In a previous work, we extended to dependent types and higher-order rewriting, the notion of "sized types" studied by several authors in the simpler framework of ML-like languages, and proved that it preserves strong normalization. The main contribution of the present paper is twofold. First, we prove that, in the Calculus of Algebraic Constructions with size annotations, the problems of type inference and type-checking are decidable, provided that the sets of constraints generated by size annotations are satisfiable and admit most general solutions. Second, we prove the latter properties for a size algebra rich enough for capturing usual induction-based definitions and much more. |
|---|
| C02 | 01 | X | | @0 001D02A04 |
|---|
| C03 | 01 | X | FRE | @0 Programmation logique @5 01 |
|---|
| C03 | 01 | X | ENG | @0 Logical programming @5 01 |
|---|
| C03 | 01 | X | SPA | @0 Programación lógica @5 01 |
|---|
| C03 | 02 | X | FRE | @0 Décidabilité @5 06 |
|---|
| C03 | 02 | X | ENG | @0 Decidability @5 06 |
|---|
| C03 | 02 | X | SPA | @0 Decidibilidad @5 06 |
|---|
| C03 | 03 | 3 | FRE | @0 Théorie type @5 07 |
|---|
| C03 | 03 | 3 | ENG | @0 Type theory @5 07 |
|---|
| C03 | 04 | X | FRE | @0 Démonstration automatique @5 08 |
|---|
| C03 | 04 | X | ENG | @0 Automatic proving @5 08 |
|---|
| C03 | 04 | X | SPA | @0 Demostración automática @5 08 |
|---|
| C03 | 05 | X | FRE | @0 Vérification programme @5 09 |
|---|
| C03 | 05 | X | ENG | @0 Program verification @5 09 |
|---|
| C03 | 05 | X | SPA | @0 Verificación programa @5 09 |
|---|
| C03 | 06 | X | FRE | @0 Automatisation @5 10 |
|---|
| C03 | 06 | X | ENG | @0 Automation @5 10 |
|---|
| C03 | 06 | X | SPA | @0 Automatización @5 10 |
|---|
| C03 | 07 | 3 | FRE | @0 Langage ML @5 11 |
|---|
| C03 | 07 | 3 | ENG | @0 ML language @5 11 |
|---|
| C03 | 08 | X | FRE | @0 Induction @5 12 |
|---|
| C03 | 08 | X | ENG | @0 Induction @5 12 |
|---|
| C03 | 08 | X | SPA | @0 Inducción @5 12 |
|---|
| C03 | 09 | X | FRE | @0 Annotation @5 18 |
|---|
| C03 | 09 | X | ENG | @0 Annotation @5 18 |
|---|
| C03 | 09 | X | SPA | @0 Anotación @5 18 |
|---|
| C03 | 10 | X | FRE | @0 Réécriture @5 19 |
|---|
| C03 | 10 | X | ENG | @0 Rewriting @5 19 |
|---|
| C03 | 10 | X | SPA | @0 Reescritura @5 19 |
|---|
| C03 | 11 | X | FRE | @0 Rho calcul @5 23 |
|---|
| C03 | 11 | X | ENG | @0 Rho calculus @5 23 |
|---|
| C03 | 11 | X | SPA | @0 Rho cálculo @5 23 |
|---|
| C03 | 12 | X | FRE | @0 Modélisation @5 24 |
|---|
| C03 | 12 | X | ENG | @0 Modeling @5 24 |
|---|
| C03 | 12 | X | SPA | @0 Modelización @5 24 |
|---|
| C03 | 13 | X | FRE | @0 Problème terminaison @5 25 |
|---|
| C03 | 13 | X | ENG | @0 Termination problem @5 25 |
|---|
| C03 | 13 | X | SPA | @0 Problema terminación @5 25 |
|---|
| C03 | 14 | X | FRE | @0 . @4 INC @5 82 |
|---|
| N21 | | | | @1 283 |
|---|
| N44 | 01 | | | @1 OTO |
|---|
| N82 | | | | @1 OTO |
|---|
|
|---|
| pR |
| A30 | 01 | 1 | ENG | @1 International workshop on computer science logic @2 19 @3 Oxford GBR @4 2005-08-22 |
|---|
| A30 | 02 | 1 | ENG | @1 EACSL. Annual conference @2 14 @3 Oxford GBR @4 2005-08-22 |
|---|
|
|---|
Format Inist (serveur)
| NO : | PASCAL 05-0409388 INIST |
|---|
| ET : | Decidability of type-checking in the calculus of algebraic constructions with size annotations |
|---|
| AU : | BLANQUI (Frédéric); ONG (Luke) |
|---|
| AF : | Laboratoire Lorrain de Recherche en Informatique et Automatique (LORIA) Institut National de Recherche en Informatique et Automatique (INRIA) 615 rue du Jardin Botanique, BP 101/54602 Villers-lès-Nancy/France (1 aut.) |
|---|
| DT : | Publication en série; Congrès; Niveau analytique |
|---|
| SO : | Lecture notes in computer science; ISSN 0302-9743; Allemagne; Da. 2005; Vol. 3634; Pp. 135-150; Bibl. 30 ref. |
|---|
| LA : | Anglais |
|---|
| EA : | Since Val Tannen's pioneering work on the combination of simply-typed A-calculus and first-order rewriting [11], many authors have contributed to this subject by extending it to richer typed A-calculi and rewriting paradigms, culminating in the Calculus of Algebraic Constructions. These works provide theoretical foundations for type-theoretic proof assistants where functions and predicates are defined by oriented higher-order equations. This kind of definitions subsumes usual inductive definitions, is easier to write and provides more automation. On the other hand, checking that such user-defined rewrite rules, when combined with β-reduction, are strongly normalizing and confluent, and preserve the decidability of type-checking, is more difficult. Most termination criteria rely on the term structure. In a previous work, we extended to dependent types and higher-order rewriting, the notion of "sized types" studied by several authors in the simpler framework of ML-like languages, and proved that it preserves strong normalization. The main contribution of the present paper is twofold. First, we prove that, in the Calculus of Algebraic Constructions with size annotations, the problems of type inference and type-checking are decidable, provided that the sets of constraints generated by size annotations are satisfiable and admit most general solutions. Second, we prove the latter properties for a size algebra rich enough for capturing usual induction-based definitions and much more. |
|---|
| CC : | 001D02A04 |
|---|
| FD : | Programmation logique; Décidabilité; Théorie type; Démonstration automatique; Vérification programme; Automatisation; Langage ML; Induction; Annotation; Réécriture; Rho calcul; Modélisation; Problème terminaison; . |
|---|
| ED : | Logical programming; Decidability; Type theory; Automatic proving; Program verification; Automation; ML language; Induction; Annotation; Rewriting; Rho calculus; Modeling; Termination problem |
|---|
| SD : | Programación lógica; Decidibilidad; Demostración automática; Verificación programa; Automatización; Inducción; Anotación; Reescritura; Rho cálculo; Modelización; Problema terminación |
|---|
| LO : | INIST-16343.354000124413180110 |
|---|
| ID : | 05-0409388 |
|---|
Links to Exploration step
Pascal:05-0409388
Le document en format XML
<record><TEI><teiHeader><fileDesc><titleStmt><title xml:lang="en" level="a">Decidability of type-checking in the calculus of algebraic constructions with size annotations</title>
<author><name sortKey="Blanqui, Frederic" sort="Blanqui, Frederic" uniqKey="Blanqui F" first="Frédéric" last="Blanqui">Frédéric Blanqui</name>
<affiliation><inist:fA14 i1="01"><s1>Laboratoire Lorrain de Recherche en Informatique et Automatique (LORIA) Institut National de Recherche en Informatique et Automatique (INRIA) 615 rue du Jardin Botanique, BP 101</s1>
<s2>54602 Villers-lès-Nancy</s2>
<s3>FRA</s3>
<sZ>1 aut.</sZ>
</inist:fA14><publicationStmt><idno type="wicri:source">INIST</idno>
<idno type="inist">05-0409388</idno>
<date when="2005">2005</date>
<idno type="stanalyst">PASCAL 05-0409388 INIST</idno>
<idno type="RBID">Pascal:05-0409388</idno>
<idno type="wicri:Area/PascalFrancis/Corpus">000519</idno>
</publicationStmt><sourceDesc><biblStruct><analytic><title xml:lang="en" level="a">Decidability of type-checking in the calculus of algebraic constructions with size annotations</title>
<author><name sortKey="Blanqui, Frederic" sort="Blanqui, Frederic" uniqKey="Blanqui F" first="Frédéric" last="Blanqui">Frédéric Blanqui</name>
<affiliation><inist:fA14 i1="01"><s1>Laboratoire Lorrain de Recherche en Informatique et Automatique (LORIA) Institut National de Recherche en Informatique et Automatique (INRIA) 615 rue du Jardin Botanique, BP 101</s1>
<s2>54602 Villers-lès-Nancy</s2>
<s3>FRA</s3>
<sZ>1 aut.</sZ>
</inist:fA14><series><title level="j" type="main">Lecture notes in computer science</title>
<idno type="ISSN">0302-9743</idno>
<imprint><date when="2005">2005</date>
</imprint><seriesStmt><title level="j" type="main">Lecture notes in computer science</title>
<idno type="ISSN">0302-9743</idno>
</seriesStmt><profileDesc><textClass><keywords scheme="KwdEn" xml:lang="en"><term>Annotation</term>
<term>Automatic proving</term>
<term>Automation</term>
<term>Decidability</term>
<term>Induction</term>
<term>Logical programming</term>
<term>ML language</term>
<term>Modeling</term>
<term>Program verification</term>
<term>Rewriting</term>
<term>Rho calculus</term>
<term>Termination problem</term>
<term>Type theory</term>
</keywords><keywords scheme="Pascal" xml:lang="fr"><term>Programmation logique</term>
<term>Décidabilité</term>
<term>Théorie type</term>
<term>Démonstration automatique</term>
<term>Vérification programme</term>
<term>Automatisation</term>
<term>Langage ML</term>
<term>Induction</term>
<term>Annotation</term>
<term>Réécriture</term>
<term>Rho calcul</term>
<term>Modélisation</term>
<term>Problème terminaison</term>
<term>.</term>
</keywords><front><div type="abstract" xml:lang="en">Since Val Tannen's pioneering work on the combination of simply-typed A-calculus and first-order rewriting [11], many authors have contributed to this subject by extending it to richer typed A-calculi and rewriting paradigms, culminating in the Calculus of Algebraic Constructions. These works provide theoretical foundations for type-theoretic proof assistants where functions and predicates are defined by oriented higher-order equations. This kind of definitions subsumes usual inductive definitions, is easier to write and provides more automation. On the other hand, checking that such user-defined rewrite rules, when combined with β-reduction, are strongly normalizing and confluent, and preserve the decidability of type-checking, is more difficult. Most termination criteria rely on the term structure. In a previous work, we extended to dependent types and higher-order rewriting, the notion of "sized types" studied by several authors in the simpler framework of ML-like languages, and proved that it preserves strong normalization. The main contribution of the present paper is twofold. First, we prove that, in the Calculus of Algebraic Constructions with size annotations, the problems of type inference and type-checking are decidable, provided that the sets of constraints generated by size annotations are satisfiable and admit most general solutions. Second, we prove the latter properties for a size algebra rich enough for capturing usual induction-based definitions and much more.</div>
</front><inist><standard h6="B"><pA><fA01 i1="01" i2="1"><s0>0302-9743</s0>
</fA01><fA05><s2>3634</s2>
</fA05><fA08 i1="01" i2="1" l="ENG"><s1>Decidability of type-checking in the calculus of algebraic constructions with size annotations</s1>
</fA08><fA09 i1="01" i2="1" l="ENG"><s1>CSL 2005 : computer science logic : Oxford, 22-25 August 2005</s1>
</fA09><fA11 i1="01" i2="1"><s1>BLANQUI (Frédéric)</s1>
</fA11><fA12 i1="01" i2="1"><s1>ONG (Luke)</s1>
<s9>ed.</s9>
</fA12><fA14 i1="01"><s1>Laboratoire Lorrain de Recherche en Informatique et Automatique (LORIA) Institut National de Recherche en Informatique et Automatique (INRIA) 615 rue du Jardin Botanique, BP 101</s1>
<s2>54602 Villers-lès-Nancy</s2>
<s3>FRA</s3>
<sZ>1 aut.</sZ>
</fA14><fA20><s1>135-150</s1>
</fA20><fA21><s1>2005</s1>
</fA21><fA23 i1="01"><s0>ENG</s0>
</fA23><fA26 i1="01"><s0>3-540-28231-9</s0>
</fA26><fA43 i1="01"><s1>INIST</s1>
<s2>16343</s2>
<s5>354000124413180110</s5>
</fA43><fA44><s0>0000</s0>
<s1>© 2005 INIST-CNRS. All rights reserved.</s1>
</fA44><fA45><s0>30 ref.</s0>
</fA45><fA47 i1="01" i2="1"><s0>05-0409388</s0>
</fA47><fA60><s1>P</s1>
<s2>C</s2>
</fA60><fA64 i1="01" i2="1"><s0>Lecture notes in computer science</s0>
</fA64><fA66 i1="01"><s0>DEU</s0>
</fA66><fC01 i1="01" l="ENG"><s0>Since Val Tannen's pioneering work on the combination of simply-typed A-calculus and first-order rewriting [11], many authors have contributed to this subject by extending it to richer typed A-calculi and rewriting paradigms, culminating in the Calculus of Algebraic Constructions. These works provide theoretical foundations for type-theoretic proof assistants where functions and predicates are defined by oriented higher-order equations. This kind of definitions subsumes usual inductive definitions, is easier to write and provides more automation. On the other hand, checking that such user-defined rewrite rules, when combined with β-reduction, are strongly normalizing and confluent, and preserve the decidability of type-checking, is more difficult. Most termination criteria rely on the term structure. In a previous work, we extended to dependent types and higher-order rewriting, the notion of "sized types" studied by several authors in the simpler framework of ML-like languages, and proved that it preserves strong normalization. The main contribution of the present paper is twofold. First, we prove that, in the Calculus of Algebraic Constructions with size annotations, the problems of type inference and type-checking are decidable, provided that the sets of constraints generated by size annotations are satisfiable and admit most general solutions. Second, we prove the latter properties for a size algebra rich enough for capturing usual induction-based definitions and much more.</s0>
</fC01><fC02 i1="01" i2="X"><s0>001D02A04</s0>
</fC02><fC03 i1="01" i2="X" l="FRE"><s0>Programmation logique</s0>
<s5>01</s5>
</fC03><fC03 i1="01" i2="X" l="ENG"><s0>Logical programming</s0>
<s5>01</s5>
</fC03><fC03 i1="01" i2="X" l="SPA"><s0>Programación lógica</s0>
<s5>01</s5>
</fC03><fC03 i1="02" i2="X" l="FRE"><s0>Décidabilité</s0>
<s5>06</s5>
</fC03><fC03 i1="02" i2="X" l="ENG"><s0>Decidability</s0>
<s5>06</s5>
</fC03><fC03 i1="02" i2="X" l="SPA"><s0>Decidibilidad</s0>
<s5>06</s5>
</fC03><fC03 i1="03" i2="3" l="FRE"><s0>Théorie type</s0>
<s5>07</s5>
</fC03><fC03 i1="03" i2="3" l="ENG"><s0>Type theory</s0>
<s5>07</s5>
</fC03><fC03 i1="04" i2="X" l="FRE"><s0>Démonstration automatique</s0>
<s5>08</s5>
</fC03><fC03 i1="04" i2="X" l="ENG"><s0>Automatic proving</s0>
<s5>08</s5>
</fC03><fC03 i1="04" i2="X" l="SPA"><s0>Demostración automática</s0>
<s5>08</s5>
</fC03><fC03 i1="05" i2="X" l="FRE"><s0>Vérification programme</s0>
<s5>09</s5>
</fC03><fC03 i1="05" i2="X" l="ENG"><s0>Program verification</s0>
<s5>09</s5>
</fC03><fC03 i1="05" i2="X" l="SPA"><s0>Verificación programa</s0>
<s5>09</s5>
</fC03><fC03 i1="06" i2="X" l="FRE"><s0>Automatisation</s0>
<s5>10</s5>
</fC03><fC03 i1="06" i2="X" l="ENG"><s0>Automation</s0>
<s5>10</s5>
</fC03><fC03 i1="06" i2="X" l="SPA"><s0>Automatización</s0>
<s5>10</s5>
</fC03><fC03 i1="07" i2="3" l="FRE"><s0>Langage ML</s0>
<s5>11</s5>
</fC03><fC03 i1="07" i2="3" l="ENG"><s0>ML language</s0>
<s5>11</s5>
</fC03><fC03 i1="08" i2="X" l="FRE"><s0>Induction</s0>
<s5>12</s5>
</fC03><fC03 i1="08" i2="X" l="ENG"><s0>Induction</s0>
<s5>12</s5>
</fC03><fC03 i1="08" i2="X" l="SPA"><s0>Inducción</s0>
<s5>12</s5>
</fC03><fC03 i1="09" i2="X" l="FRE"><s0>Annotation</s0>
<s5>18</s5>
</fC03><fC03 i1="09" i2="X" l="ENG"><s0>Annotation</s0>
<s5>18</s5>
</fC03><fC03 i1="09" i2="X" l="SPA"><s0>Anotación</s0>
<s5>18</s5>
</fC03><fC03 i1="10" i2="X" l="FRE"><s0>Réécriture</s0>
<s5>19</s5>
</fC03><fC03 i1="10" i2="X" l="ENG"><s0>Rewriting</s0>
<s5>19</s5>
</fC03><fC03 i1="10" i2="X" l="SPA"><s0>Reescritura</s0>
<s5>19</s5>
</fC03><fC03 i1="11" i2="X" l="FRE"><s0>Rho calcul</s0>
<s5>23</s5>
</fC03><fC03 i1="11" i2="X" l="ENG"><s0>Rho calculus</s0>
<s5>23</s5>
</fC03><fC03 i1="11" i2="X" l="SPA"><s0>Rho cálculo</s0>
<s5>23</s5>
</fC03><fC03 i1="12" i2="X" l="FRE"><s0>Modélisation</s0>
<s5>24</s5>
</fC03><fC03 i1="12" i2="X" l="ENG"><s0>Modeling</s0>
<s5>24</s5>
</fC03><fC03 i1="12" i2="X" l="SPA"><s0>Modelización</s0>
<s5>24</s5>
</fC03><fC03 i1="13" i2="X" l="FRE"><s0>Problème terminaison</s0>
<s5>25</s5>
</fC03><fC03 i1="13" i2="X" l="ENG"><s0>Termination problem</s0>
<s5>25</s5>
</fC03><fC03 i1="13" i2="X" l="SPA"><s0>Problema terminación</s0>
<s5>25</s5>
</fC03><fC03 i1="14" i2="X" l="FRE"><s0>.</s0>
<s4>INC</s4>
<s5>82</s5>
</fC03><fN21><s1>283</s1>
</fN21><fN44 i1="01"><s1>OTO</s1>
</fN44><fN82><s1>OTO</s1>
</fN82><pR><fA30 i1="01" i2="1" l="ENG"><s1>International workshop on computer science logic</s1>
<s2>19</s2>
<s3>Oxford GBR</s3>
<s4>2005-08-22</s4>
</fA30><fA30 i1="02" i2="1" l="ENG"><s1>EACSL. Annual conference</s1>
<s2>14</s2>
<s3>Oxford GBR</s3>
<s4>2005-08-22</s4>
</fA30><server><NO>PASCAL 05-0409388 INIST</NO>
<ET>Decidability of type-checking in the calculus of algebraic constructions with size annotations</ET>
<AU>BLANQUI (Frédéric); ONG (Luke)</AU>
<AF>Laboratoire Lorrain de Recherche en Informatique et Automatique (LORIA) Institut National de Recherche en Informatique et Automatique (INRIA) 615 rue du Jardin Botanique, BP 101/54602 Villers-lès-Nancy/France (1 aut.)</AF>
<DT>Publication en série; Congrès; Niveau analytique</DT>
<SO>Lecture notes in computer science; ISSN 0302-9743; Allemagne; Da. 2005; Vol. 3634; Pp. 135-150; Bibl. 30 ref.</SO>
<LA>Anglais</LA>
<EA>Since Val Tannen's pioneering work on the combination of simply-typed A-calculus and first-order rewriting [11], many authors have contributed to this subject by extending it to richer typed A-calculi and rewriting paradigms, culminating in the Calculus of Algebraic Constructions. These works provide theoretical foundations for type-theoretic proof assistants where functions and predicates are defined by oriented higher-order equations. This kind of definitions subsumes usual inductive definitions, is easier to write and provides more automation. On the other hand, checking that such user-defined rewrite rules, when combined with β-reduction, are strongly normalizing and confluent, and preserve the decidability of type-checking, is more difficult. Most termination criteria rely on the term structure. In a previous work, we extended to dependent types and higher-order rewriting, the notion of "sized types" studied by several authors in the simpler framework of ML-like languages, and proved that it preserves strong normalization. The main contribution of the present paper is twofold. First, we prove that, in the Calculus of Algebraic Constructions with size annotations, the problems of type inference and type-checking are decidable, provided that the sets of constraints generated by size annotations are satisfiable and admit most general solutions. Second, we prove the latter properties for a size algebra rich enough for capturing usual induction-based definitions and much more.</EA>
<CC>001D02A04</CC>
<FD>Programmation logique; Décidabilité; Théorie type; Démonstration automatique; Vérification programme; Automatisation; Langage ML; Induction; Annotation; Réécriture; Rho calcul; Modélisation; Problème terminaison; .</FD>
<ED>Logical programming; Decidability; Type theory; Automatic proving; Program verification; Automation; ML language; Induction; Annotation; Rewriting; Rho calculus; Modeling; Termination problem</ED>
<SD>Programación lógica; Decidibilidad; Demostración automática; Verificación programa; Automatización; Inducción; Anotación; Reescritura; Rho cálculo; Modelización; Problema terminación</SD>
<LO>INIST-16343.354000124413180110</LO>
<ID>05-0409388</ID>
</server>
Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/PascalFrancis/Corpus
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 000519 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/PascalFrancis/Corpus/biblio.hfd -nk 000519 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= PascalFrancis
|étape= Corpus
|type= RBID
|clé= Pascal:05-0409388
|texte= Decidability of type-checking in the calculus of algebraic constructions with size annotations
}}
| This area was generated with Dilib version V0.6.33.
Data generation: Mon Jun 10 21:56:28 2019. Site generation: Fri Feb 25 15:29:27 2022 |  |
