Proof-search in type-theoretic languages: an introduction
Identifieur interne : 009D18 ( Main/Exploration ); précédent : 009D17; suivant : 009D19Proof-search in type-theoretic languages: an introduction
Auteurs : Didier Galmiche [France] ; David J. Pym [Royaume-Uni]Source :
- Theoretical Computer Science [ 0304-3975 ] ; 2000.
Descripteurs français
- Pascal (Inist)
English descriptors
- KwdEn :
- Teeft :
- Academic press, Algebraic, Algorithm, Answer substitution, Atomic positions, Automat, Avron, Axiom, Basic idea, Boolean constraints, Cade, Cade workshop, Calculus, Cambridge university press, Category theory, Cient, Classical logic, Classical search, Classical sequent calculus, Comput, Computational, Computer, Computer science, Conf, Consequence relation, Consequence relations, Constructive program synthesis, Constructive type theory, Deductive systems, Dependent types, Electronic notes, Encoding, Erent, Formula tree, Framework, Function space, Functional programming, Functorial models, Galmiche, Girard, Herbrand, Herbrand models, Herbrand structure, Hereditary harrop formulae, Inductive, Inference rules, Interactive, Interactive theorem provers, Internal logic, Internal structure, Internat, Intuitionistic, Intuitionistic logic, Intuitionistic logics, Intuitionistic propositional logic, Intuitionistic provability, Judgement, July, Kripke, Kripke models, Lambda calculus, Lecture notes, Linear logic, Linear logic programming, Logic, Logic comput, Logic programming, Logic programming language, Logical framework, Logical frameworks, Logical systems, Matrix, Minimal logic, Modal logics, Natural deduction, Natural deduction systems, Normal proofs, Nuprl, Operational semantics, Other logics, Oxford university press, Parigot, Petri nets, Pfenning, Predicate, Predicate logic, Proc, Program synthesis, Programming, Programming language, Proof nets, Proof nets construction, Proof search, Proof system, Proof systems, Proof theory, Proof transformations, Proofsearch, Propositional, Propositional intuitionistic logic, Provability, Provable, Prover, Provers, Pure appl, Representation mechanism, Resolution calculus, Saratoga springs, Satisfaction relation, Search procedure, Search space, Semantics, Sequent, Sequent calculi, Sequent calculus, Sequents, Single publication, Springer, Structural rules, Substructural, Substructural logics, Symbolic logic, Tableau, Theorem provers, Theoret, Theoretical computer science, Typable terms, Type system, Type systems, Type theories, Type theory, Uniform proofs, Wallen.
- mix :
Abstract
Abstract: We introduce the main concepts and problems in the theory of proof-search in type-theoretic languages and survey some specific, connected topics. We do not claim to cover all of the theoretical and implementation issues in the study of proof-search in type-theoretic languages; rather, we present some key ideas and problems, starting from well-motivated points of departure such as a definition of a type-theoretic language or the relationship between languages and proof-objects. The strong connections between different proof-search methods in logics, type theories and logical frameworks, together with their impact on programming and implementation issues, are central in this context.
Url:
DOI: 10.1016/S0304-3975(99)00169-3
Affiliations:
- France, Royaume-Uni
- Angleterre, Grand Est, Grand Londres, Lorraine (région)
- Londres, Vandœuvre-lès-Nancy
- Université Henri Poincaré, Université de Londres
Links toward previous steps (curation, corpus...)
- to stream Istex, to step Corpus: 001656
- to stream Istex, to step Curation: 001637
- to stream Istex, to step Checkpoint: 001F70
- to stream Main, to step Merge: 00A298
- to stream Hal, to step Corpus: 003D90
- to stream Hal, to step Curation: 003D90
- to stream Hal, to step Checkpoint: 006177
- to stream Main, to step Merge: 00A811
- to stream PascalFrancis, to step Corpus: 000A74
- to stream PascalFrancis, to step Curation: 000008
- to stream PascalFrancis, to step Checkpoint: 000974
- to stream Main, to step Merge: 00A580
- to stream Main, to step Curation: 009D18
Le document en format XML
<record><TEI wicri:istexFullTextTei="biblStruct"><teiHeader><fileDesc><titleStmt><title>Proof-search in type-theoretic languages: an introduction</title>
<author><name sortKey="Galmiche, Didier" sort="Galmiche, Didier" uniqKey="Galmiche D" first="Didier" last="Galmiche">Didier Galmiche</name>
</author>
<author><name sortKey="Pym, David J" sort="Pym, David J" uniqKey="Pym D" first="David J." last="Pym">David J. Pym</name>
</author>
</titleStmt>
<publicationStmt><idno type="wicri:source">ISTEX</idno>
<idno type="RBID">ISTEX:60F3E329459D751A183454414CCCEB80DC4A947E</idno>
<date when="2000" year="2000">2000</date>
<idno type="doi">10.1016/S0304-3975(99)00169-3</idno>
<idno type="url">https://api.istex.fr/ark:/67375/6H6-1F1HBVPL-L/fulltext.pdf</idno>
<idno type="wicri:Area/Istex/Corpus">001656</idno>
<idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">001656</idno>
<idno type="wicri:Area/Istex/Curation">001637</idno>
<idno type="wicri:Area/Istex/Checkpoint">001F70</idno>
<idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Checkpoint">001F70</idno>
<idno type="wicri:doubleKey">0304-3975:2000:Galmiche D:proof:search:in</idno>
<idno type="wicri:Area/Main/Merge">00A298</idno>
<idno type="wicri:source">HAL</idno>
<idno type="RBID">Hal:inria-00099225</idno>
<idno type="url">https://hal.inria.fr/inria-00099225</idno>
<idno type="wicri:Area/Hal/Corpus">003D90</idno>
<idno type="wicri:Area/Hal/Curation">003D90</idno>
<idno type="wicri:Area/Hal/Checkpoint">006177</idno>
<idno type="wicri:explorRef" wicri:stream="Hal" wicri:step="Checkpoint">006177</idno>
<idno type="wicri:doubleKey">0304-3975:2000:Galmiche D:proof:search:in</idno>
<idno type="wicri:Area/Main/Merge">00A811</idno>
<idno type="wicri:source">INIST</idno>
<idno type="RBID">Pascal:00-0103215</idno>
<idno type="wicri:Area/PascalFrancis/Corpus">000A74</idno>
<idno type="wicri:Area/PascalFrancis/Curation">000008</idno>
<idno type="wicri:Area/PascalFrancis/Checkpoint">000974</idno>
<idno type="wicri:explorRef" wicri:stream="PascalFrancis" wicri:step="Checkpoint">000974</idno>
<idno type="wicri:doubleKey">0304-3975:2000:Galmiche D:proof:search:in</idno>
<idno type="wicri:Area/Main/Merge">00A580</idno>
<idno type="wicri:Area/Main/Curation">009D18</idno>
<idno type="wicri:Area/Main/Exploration">009D18</idno>
</publicationStmt>
<sourceDesc><biblStruct><analytic><title level="a">Proof-search in type-theoretic languages: an introduction</title>
<author><name sortKey="Galmiche, Didier" sort="Galmiche, Didier" uniqKey="Galmiche D" first="Didier" last="Galmiche">Didier Galmiche</name>
<affiliation wicri:level="4"><country xml:lang="fr">France</country>
<wicri:regionArea>LORIA UMR 7503, Université Henri Poincaré, Campus Scientifique – B.P. 239, F-54506 Vandoeuvre-lès-Nancy</wicri:regionArea>
<placeName><region type="region" nuts="2">Grand Est</region>
<region type="old region" nuts="2">Lorraine (région)</region>
<settlement type="city">Vandœuvre-lès-Nancy</settlement>
</placeName>
<orgName type="university">Université Henri Poincaré</orgName>
</affiliation>
<affiliation></affiliation>
<affiliation wicri:level="1"><country wicri:rule="url">France</country>
</affiliation>
</author>
<author><name sortKey="Pym, David J" sort="Pym, David J" uniqKey="Pym D" first="David J." last="Pym">David J. Pym</name>
<affiliation wicri:level="4"><country xml:lang="fr">Royaume-Uni</country>
<wicri:regionArea>Queen Mary & Westfield College, School of Mathematical Sciences, University of London, Mile End Road, London, E1 4NS</wicri:regionArea>
<orgName type="university">Université de Londres</orgName>
<placeName><settlement type="city">Londres</settlement>
<region type="country">Angleterre</region>
<region type="région" nuts="1">Grand Londres</region>
</placeName>
</affiliation>
<affiliation wicri:level="1"><country wicri:rule="url">Royaume-Uni</country>
</affiliation>
</author>
</analytic>
<monogr></monogr>
<series><title level="j">Theoretical Computer Science</title>
<title level="j" type="abbrev">TCS</title>
<idno type="ISSN">0304-3975</idno>
<imprint><publisher>ELSEVIER</publisher>
<date type="published" when="2000">2000</date>
<biblScope unit="volume">232</biblScope>
<biblScope unit="issue">1–2</biblScope>
<biblScope unit="page" from="5">5</biblScope>
<biblScope unit="page" to="53">53</biblScope>
</imprint>
<idno type="ISSN">0304-3975</idno>
</series>
</biblStruct>
</sourceDesc>
<seriesStmt><idno type="ISSN">0304-3975</idno>
</seriesStmt>
</fileDesc>
<profileDesc><textClass><keywords scheme="KwdEn" xml:lang="en"><term>Algorithm</term>
<term>Formal language</term>
<term>Logic</term>
<term>Logical framework</term>
<term>Logical programming</term>
<term>Proof search</term>
<term>Semantics</term>
<term>Type theoretic language</term>
<term>Type theory</term>
<term>Verification</term>
</keywords>
<keywords scheme="Pascal" xml:lang="fr"><term>Algorithme</term>
<term>Cadre logique</term>
<term>Langage formel</term>
<term>Langage type théorique</term>
<term>Logique</term>
<term>Programmation logique</term>
<term>Recherche preuve</term>
<term>Sémantique</term>
<term>Théorie type</term>
<term>Vérification</term>
</keywords>
<keywords scheme="Teeft" xml:lang="en"><term>Academic press</term>
<term>Algebraic</term>
<term>Algorithm</term>
<term>Answer substitution</term>
<term>Atomic positions</term>
<term>Automat</term>
<term>Avron</term>
<term>Axiom</term>
<term>Basic idea</term>
<term>Boolean constraints</term>
<term>Cade</term>
<term>Cade workshop</term>
<term>Calculus</term>
<term>Cambridge university press</term>
<term>Category theory</term>
<term>Cient</term>
<term>Classical logic</term>
<term>Classical search</term>
<term>Classical sequent calculus</term>
<term>Comput</term>
<term>Computational</term>
<term>Computer</term>
<term>Computer science</term>
<term>Conf</term>
<term>Consequence relation</term>
<term>Consequence relations</term>
<term>Constructive program synthesis</term>
<term>Constructive type theory</term>
<term>Deductive systems</term>
<term>Dependent types</term>
<term>Electronic notes</term>
<term>Encoding</term>
<term>Erent</term>
<term>Formula tree</term>
<term>Framework</term>
<term>Function space</term>
<term>Functional programming</term>
<term>Functorial models</term>
<term>Galmiche</term>
<term>Girard</term>
<term>Herbrand</term>
<term>Herbrand models</term>
<term>Herbrand structure</term>
<term>Hereditary harrop formulae</term>
<term>Inductive</term>
<term>Inference rules</term>
<term>Interactive</term>
<term>Interactive theorem provers</term>
<term>Internal logic</term>
<term>Internal structure</term>
<term>Internat</term>
<term>Intuitionistic</term>
<term>Intuitionistic logic</term>
<term>Intuitionistic logics</term>
<term>Intuitionistic propositional logic</term>
<term>Intuitionistic provability</term>
<term>Judgement</term>
<term>July</term>
<term>Kripke</term>
<term>Kripke models</term>
<term>Lambda calculus</term>
<term>Lecture notes</term>
<term>Linear logic</term>
<term>Linear logic programming</term>
<term>Logic</term>
<term>Logic comput</term>
<term>Logic programming</term>
<term>Logic programming language</term>
<term>Logical framework</term>
<term>Logical frameworks</term>
<term>Logical systems</term>
<term>Matrix</term>
<term>Minimal logic</term>
<term>Modal logics</term>
<term>Natural deduction</term>
<term>Natural deduction systems</term>
<term>Normal proofs</term>
<term>Nuprl</term>
<term>Operational semantics</term>
<term>Other logics</term>
<term>Oxford university press</term>
<term>Parigot</term>
<term>Petri nets</term>
<term>Pfenning</term>
<term>Predicate</term>
<term>Predicate logic</term>
<term>Proc</term>
<term>Program synthesis</term>
<term>Programming</term>
<term>Programming language</term>
<term>Proof nets</term>
<term>Proof nets construction</term>
<term>Proof search</term>
<term>Proof system</term>
<term>Proof systems</term>
<term>Proof theory</term>
<term>Proof transformations</term>
<term>Proofsearch</term>
<term>Propositional</term>
<term>Propositional intuitionistic logic</term>
<term>Provability</term>
<term>Provable</term>
<term>Prover</term>
<term>Provers</term>
<term>Pure appl</term>
<term>Representation mechanism</term>
<term>Resolution calculus</term>
<term>Saratoga springs</term>
<term>Satisfaction relation</term>
<term>Search procedure</term>
<term>Search space</term>
<term>Semantics</term>
<term>Sequent</term>
<term>Sequent calculi</term>
<term>Sequent calculus</term>
<term>Sequents</term>
<term>Single publication</term>
<term>Springer</term>
<term>Structural rules</term>
<term>Substructural</term>
<term>Substructural logics</term>
<term>Symbolic logic</term>
<term>Tableau</term>
<term>Theorem provers</term>
<term>Theoret</term>
<term>Theoretical computer science</term>
<term>Typable terms</term>
<term>Type system</term>
<term>Type systems</term>
<term>Type theories</term>
<term>Type theory</term>
<term>Uniform proofs</term>
<term>Wallen</term>
</keywords>
<keywords scheme="mix" xml:lang="en"><term>logical frameworks</term>
<term>logics</term>
<term>logiques</term>
<term>proof-objects</term>
<term>proof-search</term>
<term>recherche de preuves</term>
<term>semantics</term>
<term>sémantique</term>
<term>théorie des types</term>
<term>type theory</term>
<term>type-theoretic languages</term>
</keywords>
</textClass>
<langUsage><language ident="en">en</language>
</langUsage>
</profileDesc>
</teiHeader>
<front><div type="abstract" xml:lang="en">Abstract: We introduce the main concepts and problems in the theory of proof-search in type-theoretic languages and survey some specific, connected topics. We do not claim to cover all of the theoretical and implementation issues in the study of proof-search in type-theoretic languages; rather, we present some key ideas and problems, starting from well-motivated points of departure such as a definition of a type-theoretic language or the relationship between languages and proof-objects. The strong connections between different proof-search methods in logics, type theories and logical frameworks, together with their impact on programming and implementation issues, are central in this context.</div>
</front>
</TEI>
<affiliations><list><country><li>France</li>
<li>Royaume-Uni</li>
</country>
<region><li>Angleterre</li>
<li>Grand Est</li>
<li>Grand Londres</li>
<li>Lorraine (région)</li>
</region>
<settlement><li>Londres</li>
<li>Vandœuvre-lès-Nancy</li>
</settlement>
<orgName><li>Université Henri Poincaré</li>
<li>Université de Londres</li>
</orgName>
</list>
<tree><country name="France"><region name="Grand Est"><name sortKey="Galmiche, Didier" sort="Galmiche, Didier" uniqKey="Galmiche D" first="Didier" last="Galmiche">Didier Galmiche</name>
</region>
<name sortKey="Galmiche, Didier" sort="Galmiche, Didier" uniqKey="Galmiche D" first="Didier" last="Galmiche">Didier Galmiche</name>
</country>
<country name="Royaume-Uni"><region name="Angleterre"><name sortKey="Pym, David J" sort="Pym, David J" uniqKey="Pym D" first="David J." last="Pym">David J. Pym</name>
</region>
<name sortKey="Pym, David J" sort="Pym, David J" uniqKey="Pym D" first="David J." last="Pym">David J. Pym</name>
</country>
</tree>
</affiliations>
</record>
Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Main/Exploration
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 009D18 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Main/Exploration/biblio.hfd -nk 009D18 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien |wiki= Wicri/Lorraine |area= InforLorV4 |flux= Main |étape= Exploration |type= RBID |clé= ISTEX:60F3E329459D751A183454414CCCEB80DC4A947E |texte= Proof-search in type-theoretic languages: an introduction }}
This area was generated with Dilib version V0.6.33. |