Higher-order equational unification via explicit substitutions
Identifieur interne :
000C26 ( PascalFrancis/Corpus );
précédent :
000C25;
suivant :
000C27
Higher-order equational unification via explicit substitutions
Auteurs : C. Kirchner ;
C. RingeissenSource :
-
Lecture notes in computer science [ 0302-9743 ] ; 1997.
RBID : Pascal:97-0547478
Descripteurs français
English descriptors
Abstract
We show how to reduce the unification problem modulo βη-conversion and a first-order equational theory E, into a first-order unification problem in a union of two non-disjoint equational theories including E and a calculus of explicit substitutions. A rule-based unification procedure in this combined theory is described and may be viewed as an extension of the one initially designed by G. Dowek, T. Hardin and C. Kirchner for performing unification of simply typed λ-terms in a first-order setting via the λσ-calculus of explicit substitutions. Additional rules are used to deal with the interaction between E and λσ.
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 1298 |
|---|
| A08 | 01 | 1 | ENG | @1 Higher-order equational unification via explicit substitutions |
|---|
| A09 | 01 | 1 | ENG | @1 ALP '97 : algebraic and logic programming : Southampton, September 3-5, 1997 |
|---|
| A11 | 01 | 1 | | @1 KIRCHNER (C.) |
|---|
| A11 | 02 | 1 | | @1 RINGEISSEN (C.) |
|---|
| A12 | 01 | 1 | | @1 HANUS (Michael) @9 ed. |
|---|
| A12 | 02 | 1 | | @1 HEERING (jan) @9 ed. |
|---|
| A12 | 03 | 1 | | @1 MEINKE (Karl) @9 ed. |
|---|
| A14 | 01 | | | @1 INRIA-Lorraine & CRIN-CNRS, 615, rue du Jardin Botanique, BP 101 @2 54602 Villers-lès-Nancy @3 FRA @Z 1 aut. @Z 2 aut. |
|---|
| A20 | | | | @1 61-75 |
|---|
| A21 | | | | @1 1997 |
|---|
| A23 | 01 | | | @0 ENG |
|---|
| A26 | 01 | | | @0 3-540-63459-2 |
|---|
| A43 | 01 | | | @1 INIST @2 16343 @5 354000068073340050 |
|---|
| A44 | | | | @0 0000 @1 © 1997 INIST-CNRS. All rights reserved. |
|---|
| A45 | | | | @0 15 ref. |
|---|
| A47 | 01 | 1 | | @0 97-0547478 |
|---|
| A60 | | | | @1 P @2 C |
|---|
| A61 | | | | @0 A |
|---|
| A64 | 01 | 1 | | @0 Lecture notes in computer science |
|---|
| A66 | 01 | | | @0 DEU |
|---|
| A66 | 02 | | | @0 USA |
|---|
| C01 | 01 | | ENG | @0 We show how to reduce the unification problem modulo βη-conversion and a first-order equational theory E, into a first-order unification problem in a union of two non-disjoint equational theories including E and a calculus of explicit substitutions. A rule-based unification procedure in this combined theory is described and may be viewed as an extension of the one initially designed by G. Dowek, T. Hardin and C. Kirchner for performing unification of simply typed λ-terms in a first-order setting via the λσ-calculus of explicit substitutions. Additional rules are used to deal with the interaction between E and λσ. |
|---|
| C02 | 01 | X | | @0 001D02A07 |
|---|
| C03 | 01 | X | FRE | @0 Informatique théorique @5 01 |
|---|
| C03 | 01 | X | ENG | @0 Computer theory @5 01 |
|---|
| C03 | 01 | X | SPA | @0 Informática teórica @5 01 |
|---|
| C03 | 02 | X | FRE | @0 Théorie équationnelle @5 02 |
|---|
| C03 | 02 | X | ENG | @0 Equational theory @5 02 |
|---|
| C03 | 02 | X | SPA | @0 Teoría ecuaciónal @5 02 |
|---|
| C03 | 03 | X | FRE | @0 Programmation logique @5 03 |
|---|
| C03 | 03 | X | ENG | @0 Logical programming @5 03 |
|---|
| C03 | 03 | X | SPA | @0 Programación lógica @5 03 |
|---|
| C03 | 04 | X | FRE | @0 Programmation fonctionnelle @5 04 |
|---|
| C03 | 04 | X | ENG | @0 Functional programming @5 04 |
|---|
| C03 | 04 | X | SPA | @0 Programación funcional @5 04 |
|---|
| C03 | 05 | X | FRE | @0 Lambda calcul @5 05 |
|---|
| C03 | 05 | X | ENG | @0 Lambda calculus @5 05 |
|---|
| C03 | 05 | X | SPA | @0 Lambda cálculo @5 05 |
|---|
| N21 | | | | @1 342 |
|---|
|
|---|
| pR |
| A30 | 01 | 1 | ENG | @1 International conference on algebraic and logic programming @2 6 @3 Southampton GBR @4 1997-09-03 |
|---|
| A30 | 02 | 1 | ENG | @1 HOA '97 : international workshop on higher-order algebra @2 3 @3 Southampton GBR @4 1997-09-03 |
|---|
|
|---|
Format Inist (serveur)
| NO : | PASCAL 97-0547478 INIST |
|---|
| ET : | Higher-order equational unification via explicit substitutions |
|---|
| AU : | KIRCHNER (C.); RINGEISSEN (C.); HANUS (Michael); HEERING (jan); MEINKE (Karl) |
|---|
| AF : | INRIA-Lorraine & CRIN-CNRS, 615, rue du Jardin Botanique, BP 101/54602 Villers-lès-Nancy/France (1 aut., 2 aut.) |
|---|
| DT : | Publication en série; Congrès; Niveau analytique |
|---|
| SO : | Lecture notes in computer science; ISSN 0302-9743; Allemagne; Da. 1997; Vol. 1298; Pp. 61-75; Bibl. 15 ref. |
|---|
| LA : | Anglais |
|---|
| EA : | We show how to reduce the unification problem modulo βη-conversion and a first-order equational theory E, into a first-order unification problem in a union of two non-disjoint equational theories including E and a calculus of explicit substitutions. A rule-based unification procedure in this combined theory is described and may be viewed as an extension of the one initially designed by G. Dowek, T. Hardin and C. Kirchner for performing unification of simply typed λ-terms in a first-order setting via the λσ-calculus of explicit substitutions. Additional rules are used to deal with the interaction between E and λσ. |
|---|
| CC : | 001D02A07 |
|---|
| FD : | Informatique théorique; Théorie équationnelle; Programmation logique; Programmation fonctionnelle; Lambda calcul |
|---|
| ED : | Computer theory; Equational theory; Logical programming; Functional programming; Lambda calculus |
|---|
| SD : | Informática teórica; Teoría ecuaciónal; Programación lógica; Programación funcional; Lambda cálculo |
|---|
| LO : | INIST-16343.354000068073340050 |
|---|
| ID : | 97-0547478 |
|---|
Links to Exploration step
Pascal:97-0547478
Le document en format XML
<record><TEI><teiHeader><fileDesc><titleStmt><title xml:lang="en" level="a">Higher-order equational unification via explicit substitutions</title>
<author><name sortKey="Kirchner, C" sort="Kirchner, C" uniqKey="Kirchner C" first="C." last="Kirchner">C. Kirchner</name>
<affiliation><inist:fA14 i1="01"><s1>INRIA-Lorraine & CRIN-CNRS, 615, rue du Jardin Botanique, BP 101</s1>
<s2>54602 Villers-lès-Nancy</s2>
<s3>FRA</s3>
<sZ>1 aut.</sZ>
<sZ>2 aut.</sZ>
</inist:fA14><author><name sortKey="Ringeissen, C" sort="Ringeissen, C" uniqKey="Ringeissen C" first="C." last="Ringeissen">C. Ringeissen</name>
<affiliation><inist:fA14 i1="01"><s1>INRIA-Lorraine & CRIN-CNRS, 615, rue du Jardin Botanique, BP 101</s1>
<s2>54602 Villers-lès-Nancy</s2>
<s3>FRA</s3>
<sZ>1 aut.</sZ>
<sZ>2 aut.</sZ>
</inist:fA14><publicationStmt><idno type="wicri:source">INIST</idno>
<idno type="inist">97-0547478</idno>
<date when="1997">1997</date>
<idno type="stanalyst">PASCAL 97-0547478 INIST</idno>
<idno type="RBID">Pascal:97-0547478</idno>
<idno type="wicri:Area/PascalFrancis/Corpus">000C26</idno>
</publicationStmt><sourceDesc><biblStruct><analytic><title xml:lang="en" level="a">Higher-order equational unification via explicit substitutions</title>
<author><name sortKey="Kirchner, C" sort="Kirchner, C" uniqKey="Kirchner C" first="C." last="Kirchner">C. Kirchner</name>
<affiliation><inist:fA14 i1="01"><s1>INRIA-Lorraine & CRIN-CNRS, 615, rue du Jardin Botanique, BP 101</s1>
<s2>54602 Villers-lès-Nancy</s2>
<s3>FRA</s3>
<sZ>1 aut.</sZ>
<sZ>2 aut.</sZ>
</inist:fA14><author><name sortKey="Ringeissen, C" sort="Ringeissen, C" uniqKey="Ringeissen C" first="C." last="Ringeissen">C. Ringeissen</name>
<affiliation><inist:fA14 i1="01"><s1>INRIA-Lorraine & CRIN-CNRS, 615, rue du Jardin Botanique, BP 101</s1>
<s2>54602 Villers-lès-Nancy</s2>
<s3>FRA</s3>
<sZ>1 aut.</sZ>
<sZ>2 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="1997">1997</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>Computer theory</term>
<term>Equational theory</term>
<term>Functional programming</term>
<term>Lambda calculus</term>
<term>Logical programming</term>
</keywords><keywords scheme="Pascal" xml:lang="fr"><term>Informatique théorique</term>
<term>Théorie équationnelle</term>
<term>Programmation logique</term>
<term>Programmation fonctionnelle</term>
<term>Lambda calcul</term>
</keywords><front><div type="abstract" xml:lang="en">We show how to reduce the unification problem modulo βη-conversion and a first-order equational theory E, into a first-order unification problem in a union of two non-disjoint equational theories including E and a calculus of explicit substitutions. A rule-based unification procedure in this combined theory is described and may be viewed as an extension of the one initially designed by G. Dowek, T. Hardin and C. Kirchner for performing unification of simply typed λ-terms in a first-order setting via the λσ-calculus of explicit substitutions. Additional rules are used to deal with the interaction between E and λσ.</div>
</front><inist><standard h6="B"><pA><fA01 i1="01" i2="1"><s0>0302-9743</s0>
</fA01><fA05><s2>1298</s2>
</fA05><fA08 i1="01" i2="1" l="ENG"><s1>Higher-order equational unification via explicit substitutions</s1>
</fA08><fA09 i1="01" i2="1" l="ENG"><s1>ALP '97 : algebraic and logic programming : Southampton, September 3-5, 1997</s1>
</fA09><fA11 i1="01" i2="1"><s1>KIRCHNER (C.)</s1>
</fA11><fA11 i1="02" i2="1"><s1>RINGEISSEN (C.)</s1>
</fA11><fA12 i1="01" i2="1"><s1>HANUS (Michael)</s1>
<s9>ed.</s9>
</fA12><fA12 i1="02" i2="1"><s1>HEERING (jan)</s1>
<s9>ed.</s9>
</fA12><fA12 i1="03" i2="1"><s1>MEINKE (Karl)</s1>
<s9>ed.</s9>
</fA12><fA14 i1="01"><s1>INRIA-Lorraine & CRIN-CNRS, 615, rue du Jardin Botanique, BP 101</s1>
<s2>54602 Villers-lès-Nancy</s2>
<s3>FRA</s3>
<sZ>1 aut.</sZ>
<sZ>2 aut.</sZ>
</fA14><fA20><s1>61-75</s1>
</fA20><fA21><s1>1997</s1>
</fA21><fA23 i1="01"><s0>ENG</s0>
</fA23><fA26 i1="01"><s0>3-540-63459-2</s0>
</fA26><fA43 i1="01"><s1>INIST</s1>
<s2>16343</s2>
<s5>354000068073340050</s5>
</fA43><fA44><s0>0000</s0>
<s1>© 1997 INIST-CNRS. All rights reserved.</s1>
</fA44><fA45><s0>15 ref.</s0>
</fA45><fA47 i1="01" i2="1"><s0>97-0547478</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><fA66 i1="02"><s0>USA</s0>
</fA66><fC01 i1="01" l="ENG"><s0>We show how to reduce the unification problem modulo βη-conversion and a first-order equational theory E, into a first-order unification problem in a union of two non-disjoint equational theories including E and a calculus of explicit substitutions. A rule-based unification procedure in this combined theory is described and may be viewed as an extension of the one initially designed by G. Dowek, T. Hardin and C. Kirchner for performing unification of simply typed λ-terms in a first-order setting via the λσ-calculus of explicit substitutions. Additional rules are used to deal with the interaction between E and λσ.</s0>
</fC01><fC02 i1="01" i2="X"><s0>001D02A07</s0>
</fC02><fC03 i1="01" i2="X" l="FRE"><s0>Informatique théorique</s0>
<s5>01</s5>
</fC03><fC03 i1="01" i2="X" l="ENG"><s0>Computer theory</s0>
<s5>01</s5>
</fC03><fC03 i1="01" i2="X" l="SPA"><s0>Informática teórica</s0>
<s5>01</s5>
</fC03><fC03 i1="02" i2="X" l="FRE"><s0>Théorie équationnelle</s0>
<s5>02</s5>
</fC03><fC03 i1="02" i2="X" l="ENG"><s0>Equational theory</s0>
<s5>02</s5>
</fC03><fC03 i1="02" i2="X" l="SPA"><s0>Teoría ecuaciónal</s0>
<s5>02</s5>
</fC03><fC03 i1="03" i2="X" l="FRE"><s0>Programmation logique</s0>
<s5>03</s5>
</fC03><fC03 i1="03" i2="X" l="ENG"><s0>Logical programming</s0>
<s5>03</s5>
</fC03><fC03 i1="03" i2="X" l="SPA"><s0>Programación lógica</s0>
<s5>03</s5>
</fC03><fC03 i1="04" i2="X" l="FRE"><s0>Programmation fonctionnelle</s0>
<s5>04</s5>
</fC03><fC03 i1="04" i2="X" l="ENG"><s0>Functional programming</s0>
<s5>04</s5>
</fC03><fC03 i1="04" i2="X" l="SPA"><s0>Programación funcional</s0>
<s5>04</s5>
</fC03><fC03 i1="05" i2="X" l="FRE"><s0>Lambda calcul</s0>
<s5>05</s5>
</fC03><fC03 i1="05" i2="X" l="ENG"><s0>Lambda calculus</s0>
<s5>05</s5>
</fC03><fC03 i1="05" i2="X" l="SPA"><s0>Lambda cálculo</s0>
<s5>05</s5>
</fC03><fN21><s1>342</s1>
</fN21><pR><fA30 i1="01" i2="1" l="ENG"><s1>International conference on algebraic and logic programming</s1>
<s2>6</s2>
<s3>Southampton GBR</s3>
<s4>1997-09-03</s4>
</fA30><fA30 i1="02" i2="1" l="ENG"><s1>HOA '97 : international workshop on higher-order algebra</s1>
<s2>3</s2>
<s3>Southampton GBR</s3>
<s4>1997-09-03</s4>
</fA30><server><NO>PASCAL 97-0547478 INIST</NO>
<ET>Higher-order equational unification via explicit substitutions</ET>
<AU>KIRCHNER (C.); RINGEISSEN (C.); HANUS (Michael); HEERING (jan); MEINKE (Karl)</AU>
<AF>INRIA-Lorraine & CRIN-CNRS, 615, rue du Jardin Botanique, BP 101/54602 Villers-lès-Nancy/France (1 aut., 2 aut.)</AF>
<DT>Publication en série; Congrès; Niveau analytique</DT>
<SO>Lecture notes in computer science; ISSN 0302-9743; Allemagne; Da. 1997; Vol. 1298; Pp. 61-75; Bibl. 15 ref.</SO>
<LA>Anglais</LA>
<EA>We show how to reduce the unification problem modulo βη-conversion and a first-order equational theory E, into a first-order unification problem in a union of two non-disjoint equational theories including E and a calculus of explicit substitutions. A rule-based unification procedure in this combined theory is described and may be viewed as an extension of the one initially designed by G. Dowek, T. Hardin and C. Kirchner for performing unification of simply typed λ-terms in a first-order setting via the λσ-calculus of explicit substitutions. Additional rules are used to deal with the interaction between E and λσ.</EA>
<CC>001D02A07</CC>
<FD>Informatique théorique; Théorie équationnelle; Programmation logique; Programmation fonctionnelle; Lambda calcul</FD>
<ED>Computer theory; Equational theory; Logical programming; Functional programming; Lambda calculus</ED>
<SD>Informática teórica; Teoría ecuaciónal; Programación lógica; Programación funcional; Lambda cálculo</SD>
<LO>INIST-16343.354000068073340050</LO>
<ID>97-0547478</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 000C26 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/PascalFrancis/Corpus/biblio.hfd -nk 000C26 | 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:97-0547478
|texte= Higher-order equational unification via explicit substitutions
}}
| 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 |  |
