Proof-search in type-theoretic languages: an introduction
Identifieur interne : 001656 ( Istex/Corpus ); précédent : 001655; suivant : 001657Proof-search in type-theoretic languages: an introduction
Auteurs : Didier Galmiche ; David J. PymSource :
- Theoretical Computer Science [ 0304-3975 ] ; 2000.
English descriptors
- 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.
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
Links to Exploration step
ISTEX:60F3E329459D751A183454414CCCEB80DC4A947ELe 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><affiliation><mods:affiliation>LORIA UMR 7503, Université Henri Poincaré, Campus Scientifique – B.P. 239, F-54506 Vandoeuvre-lès-Nancy, France</mods:affiliation></affiliation><affiliation><mods:affiliation>Corresponding author</mods:affiliation></affiliation><affiliation><mods:affiliation>E-mail: didier.galmiche@loria.fr</mods:affiliation></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><mods:affiliation>Queen Mary & Westfield College, School of Mathematical Sciences, University of London, Mile End Road, London, E1 4NS, UK</mods:affiliation></affiliation><affiliation><mods:affiliation>E-mail: david.pym@dcs.qmw.ac.uk</mods:affiliation></affiliation></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></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><mods:affiliation>LORIA UMR 7503, Université Henri Poincaré, Campus Scientifique – B.P. 239, F-54506 Vandoeuvre-lès-Nancy, France</mods:affiliation></affiliation><affiliation><mods:affiliation>Corresponding author</mods:affiliation></affiliation><affiliation><mods:affiliation>E-mail: didier.galmiche@loria.fr</mods:affiliation></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><mods:affiliation>Queen Mary & Westfield College, School of Mathematical Sciences, University of London, Mile End Road, London, E1 4NS, UK</mods:affiliation></affiliation><affiliation><mods:affiliation>E-mail: david.pym@dcs.qmw.ac.uk</mods:affiliation></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="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></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><istex><corpusName>elsevier</corpusName><keywords><teeft><json:string>calculus</json:string><json:string>semantics</json:string><json:string>intuitionistic</json:string><json:string>sequent</json:string><json:string>galmiche</json:string><json:string>theoretical computer science</json:string><json:string>linear logic</json:string><json:string>lecture notes</json:string><json:string>propositional</json:string><json:string>logic programming</json:string><json:string>intuitionistic logic</json:string><json:string>computer science</json:string><json:string>comput</json:string><json:string>provability</json:string><json:string>springer</json:string><json:string>type theory</json:string><json:string>erent</json:string><json:string>kripke</json:string><json:string>logical frameworks</json:string><json:string>sequents</json:string><json:string>conf</json:string><json:string>internat</json:string><json:string>predicate</json:string><json:string>substructural</json:string><json:string>inductive</json:string><json:string>july</json:string><json:string>logical framework</json:string><json:string>classical logic</json:string><json:string>provable</json:string><json:string>judgement</json:string><json:string>sequent calculus</json:string><json:string>theoret</json:string><json:string>encoding</json:string><json:string>wallen</json:string><json:string>herbrand</json:string><json:string>consequence relation</json:string><json:string>logic</json:string><json:string>proof nets</json:string><json:string>programming</json:string><json:string>inference rules</json:string><json:string>proof theory</json:string><json:string>natural deduction</json:string><json:string>parigot</json:string><json:string>pfenning</json:string><json:string>proofsearch</json:string><json:string>girard</json:string><json:string>prover</json:string><json:string>cambridge university press</json:string><json:string>sequent calculi</json:string><json:string>logic programming language</json:string><json:string>algorithm</json:string><json:string>automat</json:string><json:string>avron</json:string><json:string>proc</json:string><json:string>cade workshop</json:string><json:string>cient</json:string><json:string>symbolic logic</json:string><json:string>operational semantics</json:string><json:string>deductive systems</json:string><json:string>nuprl</json:string><json:string>interactive</json:string><json:string>cade</json:string><json:string>search space</json:string><json:string>provers</json:string><json:string>matrix</json:string><json:string>oxford university press</json:string><json:string>intuitionistic propositional logic</json:string><json:string>program synthesis</json:string><json:string>uniform proofs</json:string><json:string>proof transformations</json:string><json:string>basic idea</json:string><json:string>functional programming</json:string><json:string>logic comput</json:string><json:string>pure appl</json:string><json:string>consequence relations</json:string><json:string>formula tree</json:string><json:string>electronic notes</json:string><json:string>proof systems</json:string><json:string>satisfaction relation</json:string><json:string>hereditary harrop formulae</json:string><json:string>kripke models</json:string><json:string>dependent types</json:string><json:string>petri nets</json:string><json:string>natural deduction systems</json:string><json:string>algebraic</json:string><json:string>axiom</json:string><json:string>predicate logic</json:string><json:string>theorem provers</json:string><json:string>classical sequent calculus</json:string><json:string>internal structure</json:string><json:string>representation mechanism</json:string><json:string>category theory</json:string><json:string>resolution calculus</json:string><json:string>proof system</json:string><json:string>internal logic</json:string><json:string>intuitionistic provability</json:string><json:string>type system</json:string><json:string>function space</json:string><json:string>substructural logics</json:string><json:string>modal logics</json:string><json:string>logical systems</json:string><json:string>programming language</json:string><json:string>computational</json:string><json:string>tableau</json:string><json:string>computer</json:string><json:string>herbrand models</json:string><json:string>herbrand structure</json:string><json:string>answer substitution</json:string><json:string>linear logic programming</json:string><json:string>proof nets construction</json:string><json:string>boolean constraints</json:string><json:string>constructive program synthesis</json:string><json:string>constructive type theory</json:string><json:string>propositional intuitionistic logic</json:string><json:string>interactive theorem provers</json:string><json:string>normal proofs</json:string><json:string>functorial models</json:string><json:string>atomic positions</json:string><json:string>search procedure</json:string><json:string>classical search</json:string><json:string>other logics</json:string><json:string>typable terms</json:string><json:string>lambda calculus</json:string><json:string>intuitionistic logics</json:string><json:string>minimal logic</json:string><json:string>type systems</json:string><json:string>academic press</json:string><json:string>saratoga springs</json:string><json:string>proof search</json:string><json:string>structural rules</json:string><json:string>type theories</json:string><json:string>single publication</json:string><json:string>framework</json:string><json:string>constraint</json:string><json:string>proof</json:string><json:string>substitution</json:string><json:string>derivation</json:string></teeft></keywords><author><json:item><name>Didier Galmiche</name><affiliations><json:string>LORIA UMR 7503, Université Henri Poincaré, Campus Scientifique – B.P. 239, F-54506 Vandoeuvre-lès-Nancy, France</json:string><json:string>Corresponding author</json:string><json:string>E-mail: didier.galmiche@loria.fr</json:string></affiliations></json:item><json:item><name>David J. Pym</name><affiliations><json:string>Queen Mary & Westfield College, School of Mathematical Sciences, University of London, Mile End Road, London, E1 4NS, UK</json:string><json:string>E-mail: david.pym@dcs.qmw.ac.uk</json:string></affiliations></json:item></author><subject><json:item><lang><json:string>eng</json:string></lang><value>Logics</value></json:item><json:item><lang><json:string>eng</json:string></lang><value>Proof-search</value></json:item><json:item><lang><json:string>eng</json:string></lang><value>Type theory</value></json:item><json:item><lang><json:string>eng</json:string></lang><value>Semantics</value></json:item><json:item><lang><json:string>eng</json:string></lang><value>Logical frameworks</value></json:item><json:item><lang><json:string>eng</json:string></lang><value>Type-theoretic languages</value></json:item><json:item><lang><json:string>eng</json:string></lang><value>Proof-objects</value></json:item></subject><arkIstex>ark:/67375/6H6-1F1HBVPL-L</arkIstex><language><json:string>eng</json:string></language><originalGenre><json:string>Full-length article</json:string></originalGenre><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.</abstract><qualityIndicators><score>8.2</score><pdfWordCount>22010</pdfWordCount><pdfCharCount>124154</pdfCharCount><pdfVersion>1.2</pdfVersion><pdfPageCount>49</pdfPageCount><pdfPageSize>408 x 660 pts</pdfPageSize><refBibsNative>true</refBibsNative><abstractWordCount>100</abstractWordCount><abstractCharCount>700</abstractCharCount><keywordCount>7</keywordCount></qualityIndicators><title>Proof-search in type-theoretic languages: an introduction</title><pii><json:string>S0304-3975(99)00169-3</json:string></pii><genre><json:string>research-article</json:string></genre><host><title>Theoretical Computer Science</title><language><json:string>unknown</json:string></language><publicationDate>2000</publicationDate><issn><json:string>0304-3975</json:string></issn><pii><json:string>S0304-3975(00)X0125-9</json:string></pii><volume>232</volume><issue>1–2</issue><pages><first>5</first><last>53</last></pages><genre><json:string>journal</json:string></genre></host><namedEntities><unitex><date><json:string>2000</json:string></date><geogName><json:string>ILL</json:string></geogName><orgName><json:string>UK Abstract We</json:string></orgName><orgName_funder></orgName_funder><orgName_provider></orgName_provider><persName><json:string>Voronkov</json:string><json:string>Dyckho</json:string><json:string>Pfenning</json:string><json:string>Pym</json:string><json:string>Queen Mary</json:string><json:string>D.J. Pym</json:string><json:string>To</json:string><json:string>Wallen</json:string><json:string>Maurice Nivat</json:string><json:string>S. L Originally</json:string><json:string>Henri PoincarÃ</json:string><json:string>Ishtiaq</json:string><json:string>Avron</json:string><json:string>D. Galmiche</json:string><json:string>Dummett</json:string></persName><placeName><json:string>France</json:string><json:string>Monotonicity</json:string></placeName><ref_url></ref_url><ref_bibl><json:string>[67, 69, 107, 109, 113, 142, 152]</json:string><json:string>[61]</json:string><json:string>[159]</json:string><json:string>[7, 40, 73, 143, 151]</json:string><json:string>[113]</json:string><json:string>[132]</json:string><json:string>[11, 72, 151, 141]</json:string><json:string>[151]</json:string><json:string>[70, 11, 151]</json:string><json:string>[170]</json:string><json:string>[171, 69]</json:string><json:string>[23]</json:string><json:string>[167]</json:string><json:string>[116, 147, 115, 149, 150, 153]</json:string><json:string>[72, 151, 140, 132]</json:string><json:string>[29]</json:string><json:string>[118]</json:string><json:string>[6]</json:string><json:string>[137]</json:string><json:string>[156]</json:string><json:string>[141, 86, 85]</json:string><json:string>[110]</json:string><json:string>[93]</json:string><json:string>[81, 80]</json:string><json:string>[126]</json:string><json:string>[66]</json:string><json:string>[121, 87]</json:string><json:string>[35, 127]</json:string><json:string>[116, 147, 149, 150, 153]</json:string><json:string>[8]</json:string><json:string>[134]</json:string><json:string>[123, 124, 101]</json:string><json:string>[17]</json:string><json:string>[172]</json:string><json:string>[132, 133]</json:string><json:string>[104]</json:string><json:string>[169]</json:string><json:string>[1]</json:string><json:string>[143, 152]</json:string><json:string>[161]</json:string><json:string>[148, 86]</json:string><json:string>[65, 128]</json:string><json:string>[10]</json:string><json:string>[139]</json:string><json:string>[158]</json:string><json:string>[112]</json:string><json:string>[131]</json:string><json:string>[49]</json:string><json:string>[109]</json:string><json:string>[128]</json:string><json:string>[3]</json:string><json:string>[101]</json:string><json:string>[166]</json:string><json:string>[120]</json:string><json:string>Avron et al. [12]</json:string><json:string>[142, 68]</json:string><json:string>[83, 84]</json:string><json:string>[117]</json:string><json:string>[136]</json:string><json:string>[97]</json:string><json:string>[116, 147, 150]</json:string><json:string>Bundy et al.</json:string><json:string>[24, 25]</json:string><json:string>[106]</json:string><json:string>[5]</json:string><json:string>[125]</json:string><json:string>[17, 170]</json:string><json:string>[26]</json:string><json:string>[163]</json:string><json:string>[142, 171, 69]</json:string><json:string>[114]</json:string><json:string>[133]</json:string><json:string>[100, 36]</json:string><json:string>[151, 143, 152, 45]</json:string><json:string>[96]</json:string><json:string>[168]</json:string><json:string>[122]</json:string><json:string>[141]</json:string><json:string>[140, 141, 151]</json:string><json:string>[152, 143, 151]</json:string><json:string>[47]</json:string><json:string>[138]</json:string><json:string>[157]</json:string><json:string>[111]</json:string><json:string>[39, 90]</json:string><json:string>[108]</json:string><json:string>[127]</json:string><json:string>[69, 171]</json:string><json:string>[115, 116, 147]</json:string><json:string>[165]</json:string><json:string>[95]</json:string><json:string>[91, 141, 154, 155]</json:string><json:string>[135]</json:string><json:string>[2]</json:string><json:string>[46]</json:string><json:string>[11, 72, 151]</json:string><json:string>[42, 154, 155, 170]</json:string><json:string>[105]</json:string><json:string>[124]</json:string><json:string>[143]</json:string><json:string>[19]</json:string><json:string>[162]</json:string></ref_bibl><bibl></bibl></unitex></namedEntities><ark><json:string>ark:/67375/6H6-1F1HBVPL-L</json:string></ark><categories><wos><json:string>1 - science</json:string><json:string>2 - computer science, theory & methods</json:string></wos><scienceMetrix><json:string>1 - applied sciences</json:string><json:string>2 - information & communication technologies</json:string><json:string>3 - computation theory & mathematics</json:string></scienceMetrix><scopus><json:string>1 - Physical Sciences</json:string><json:string>2 - Computer Science</json:string><json:string>3 - General Computer Science</json:string><json:string>1 - Physical Sciences</json:string><json:string>2 - Mathematics</json:string><json:string>3 - Theoretical Computer Science</json:string></scopus><inist><json:string>1 - sciences humaines et sociales</json:string></inist></categories><publicationDate>2000</publicationDate><copyrightDate>2000</copyrightDate><doi><json:string>10.1016/S0304-3975(99)00169-3</json:string></doi><id>60F3E329459D751A183454414CCCEB80DC4A947E</id><score>1</score><fulltext><json:item><extension>pdf</extension><original>true</original><mimetype>application/pdf</mimetype><uri>https://api.istex.fr/ark:/67375/6H6-1F1HBVPL-L/fulltext.pdf</uri></json:item><json:item><extension>zip</extension><original>false</original><mimetype>application/zip</mimetype><uri>https://api.istex.fr/ark:/67375/6H6-1F1HBVPL-L/bundle.zip</uri></json:item><istex:fulltextTEI uri="https://api.istex.fr/ark:/67375/6H6-1F1HBVPL-L/fulltext.tei"><teiHeader><fileDesc><titleStmt><title level="a">Proof-search in type-theoretic languages: an introduction</title></titleStmt><publicationStmt><authority>ISTEX</authority><publisher scheme="https://scientific-publisher.data.istex.fr">ELSEVIER</publisher><availability><licence><p>©2000 Elsevier Science B.V.</p></licence><p scheme="https://loaded-corpus.data.istex.fr/ark:/67375/XBH-HKKZVM7B-M">elsevier</p></availability><date>2000</date></publicationStmt><notesStmt><note type="research-article" scheme="https://content-type.data.istex.fr/ark:/67375/XTP-1JC4F85T-7">research-article</note><note type="journal" scheme="https://publication-type.data.istex.fr/ark:/67375/JMC-0GLKJH51-B">journal</note></notesStmt><sourceDesc><biblStruct type="inbook"><analytic><title level="a">Proof-search in type-theoretic languages: an introduction</title><author xml:id="author-0000"><persName><forename type="first">Didier</forename><surname>Galmiche</surname></persName><email>didier.galmiche@loria.fr</email><affiliation>LORIA UMR 7503, Université Henri Poincaré, Campus Scientifique – B.P. 239, F-54506 Vandoeuvre-lès-Nancy, France</affiliation><affiliation>Corresponding author</affiliation></author><author xml:id="author-0001"><persName><forename type="first">David J.</forename><surname>Pym</surname></persName><email>david.pym@dcs.qmw.ac.uk</email><affiliation>Queen Mary & Westfield College, School of Mathematical Sciences, University of London, Mile End Road, London, E1 4NS, UK</affiliation></author><idno type="istex">60F3E329459D751A183454414CCCEB80DC4A947E</idno><idno type="ark">ark:/67375/6H6-1F1HBVPL-L</idno><idno type="DOI">10.1016/S0304-3975(99)00169-3</idno><idno type="PII">S0304-3975(99)00169-3</idno></analytic><monogr><title level="j">Theoretical Computer Science</title><title level="j" type="abbrev">TCS</title><idno type="pISSN">0304-3975</idno><idno type="PII">S0304-3975(00)X0125-9</idno><imprint><publisher>ELSEVIER</publisher><date type="published" when="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></monogr></biblStruct></sourceDesc></fileDesc><profileDesc><creation><date>2000</date></creation><langUsage><language ident="en">en</language></langUsage><abstract xml:lang="en"><p>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.</p></abstract><textClass><keywords scheme="keyword"><list><head>Keywords</head><item><term>Logics</term></item><item><term>Proof-search</term></item><item><term>Type theory</term></item><item><term>Semantics</term></item><item><term>Logical frameworks</term></item><item><term>Type-theoretic languages</term></item><item><term>Proof-objects</term></item></list></keywords></textClass></profileDesc><revisionDesc><change when="2000">Published</change></revisionDesc></teiHeader></istex:fulltextTEI><json:item><extension>txt</extension><original>false</original><mimetype>text/plain</mimetype><uri>https://api.istex.fr/ark:/67375/6H6-1F1HBVPL-L/fulltext.txt</uri></json:item></fulltext><metadata><istex:metadataXml wicri:clean="Elsevier, elements deleted: tail"><istex:xmlDeclaration>version="1.0" encoding="utf-8"</istex:xmlDeclaration><istex:docType PUBLIC="-//ES//DTD journal article DTD version 4.5.2//EN//XML" URI="art452.dtd" name="istex:docType"></istex:docType><istex:document><converted-article version="4.5.2" docsubtype="fla"><item-info><jid>TCS</jid><aid>3318</aid><ce:pii>S0304-3975(99)00169-3</ce:pii><ce:doi>10.1016/S0304-3975(99)00169-3</ce:doi><ce:copyright type="full-transfer" year="2000">Elsevier Science B.V.</ce:copyright></item-info><head><ce:title>Proof-search in type-theoretic languages: an introduction</ce:title><ce:author-group><ce:author><ce:given-name>Didier</ce:given-name><ce:surname>Galmiche</ce:surname><ce:cross-ref refid="AFF1"><ce:sup>a</ce:sup></ce:cross-ref><ce:cross-ref refid="CORR1">*</ce:cross-ref><ce:e-address>didier.galmiche@loria.fr</ce:e-address></ce:author><ce:author><ce:given-name>David J.</ce:given-name><ce:surname>Pym</ce:surname><ce:cross-ref refid="AFF2"><ce:sup>b</ce:sup></ce:cross-ref><ce:e-address>david.pym@dcs.qmw.ac.uk</ce:e-address></ce:author><ce:affiliation id="AFF1"><ce:label>a</ce:label><ce:textfn>LORIA UMR 7503, Université Henri Poincaré, Campus Scientifique – B.P. 239, F-54506 Vandoeuvre-lès-Nancy, France</ce:textfn></ce:affiliation><ce:affiliation id="AFF2"><ce:label>b</ce:label><ce:textfn>Queen Mary & Westfield College, School of Mathematical Sciences, University of London, Mile End Road, London, E1 4NS, UK</ce:textfn></ce:affiliation><ce:correspondence id="CORR1"><ce:label>*</ce:label><ce:text>Corresponding author</ce:text></ce:correspondence></ce:author-group><ce:abstract><ce:section-title>Abstract</ce:section-title><ce:abstract-sec><ce:simple-para>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.</ce:simple-para></ce:abstract-sec></ce:abstract><ce:keywords class="keyword"><ce:section-title>Keywords</ce:section-title><ce:keyword><ce:text>Logics</ce:text></ce:keyword><ce:keyword><ce:text>Proof-search</ce:text></ce:keyword><ce:keyword><ce:text>Type theory</ce:text></ce:keyword><ce:keyword><ce:text>Semantics</ce:text></ce:keyword><ce:keyword><ce:text>Logical frameworks</ce:text></ce:keyword><ce:keyword><ce:text>Type-theoretic languages</ce:text></ce:keyword><ce:keyword><ce:text>Proof-objects</ce:text></ce:keyword></ce:keywords></head></converted-article></istex:document></istex:metadataXml><mods version="3.6"><titleInfo><title>Proof-search in type-theoretic languages: an introduction</title></titleInfo><titleInfo type="alternative" contentType="CDATA"><title>Proof-search in type-theoretic languages: an introduction</title></titleInfo><name type="personal"><namePart type="given">Didier</namePart><namePart type="family">Galmiche</namePart><affiliation>LORIA UMR 7503, Université Henri Poincaré, Campus Scientifique – B.P. 239, F-54506 Vandoeuvre-lès-Nancy, France</affiliation><affiliation>Corresponding author</affiliation><affiliation>E-mail: didier.galmiche@loria.fr</affiliation><role><roleTerm type="text">author</roleTerm></role></name><name type="personal"><namePart type="given">David J.</namePart><namePart type="family">Pym</namePart><affiliation>Queen Mary & Westfield College, School of Mathematical Sciences, University of London, Mile End Road, London, E1 4NS, UK</affiliation><affiliation>E-mail: david.pym@dcs.qmw.ac.uk</affiliation><role><roleTerm type="text">author</roleTerm></role></name><typeOfResource>text</typeOfResource><genre type="research-article" displayLabel="Full-length article" authority="ISTEX" authorityURI="https://content-type.data.istex.fr" valueURI="https://content-type.data.istex.fr/ark:/67375/XTP-1JC4F85T-7">research-article</genre><originInfo><publisher>ELSEVIER</publisher><dateIssued encoding="w3cdtf">2000</dateIssued><copyrightDate encoding="w3cdtf">2000</copyrightDate></originInfo><language><languageTerm type="code" authority="iso639-2b">eng</languageTerm><languageTerm type="code" authority="rfc3066">en</languageTerm></language><abstract 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.</abstract><subject><genre>Keywords</genre><topic>Logics</topic><topic>Proof-search</topic><topic>Type theory</topic><topic>Semantics</topic><topic>Logical frameworks</topic><topic>Type-theoretic languages</topic><topic>Proof-objects</topic></subject><relatedItem type="host"><titleInfo><title>Theoretical Computer Science</title></titleInfo><titleInfo type="abbreviated"><title>TCS</title></titleInfo><genre type="journal" authority="ISTEX" authorityURI="https://publication-type.data.istex.fr" valueURI="https://publication-type.data.istex.fr/ark:/67375/JMC-0GLKJH51-B">journal</genre><originInfo><publisher>ELSEVIER</publisher><dateIssued encoding="w3cdtf">2000</dateIssued></originInfo><identifier type="ISSN">0304-3975</identifier><identifier type="PII">S0304-3975(00)X0125-9</identifier><part><date>2000</date><detail type="volume"><number>232</number><caption>vol.</caption></detail><detail type="issue"><number>1–2</number><caption>no.</caption></detail><extent unit="issue-pages"><start>1</start><end>336</end></extent><extent unit="pages"><start>5</start><end>53</end></extent></part></relatedItem><identifier type="istex">60F3E329459D751A183454414CCCEB80DC4A947E</identifier><identifier type="ark">ark:/67375/6H6-1F1HBVPL-L</identifier><identifier type="DOI">10.1016/S0304-3975(99)00169-3</identifier><identifier type="PII">S0304-3975(99)00169-3</identifier><accessCondition type="use and reproduction" contentType="copyright">©2000 Elsevier Science B.V.</accessCondition><recordInfo><recordContentSource authority="ISTEX" authorityURI="https://loaded-corpus.data.istex.fr" valueURI="https://loaded-corpus.data.istex.fr/ark:/67375/XBH-HKKZVM7B-M">elsevier</recordContentSource><recordOrigin>Elsevier Science B.V., ©2000</recordOrigin></recordInfo></mods><json:item><extension>json</extension><original>false</original><mimetype>application/json</mimetype><uri>https://api.istex.fr/ark:/67375/6H6-1F1HBVPL-L/record.json</uri></json:item></metadata><serie></serie></istex></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Istex/Corpus
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 001656 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Istex/Corpus/biblio.hfd -nk 001656 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= Istex
|étape= Corpus
|type= RBID
|clé= ISTEX:60F3E329459D751A183454414CCCEB80DC4A947E
|texte= Proof-search in type-theoretic languages: an introduction
}}
| This area was generated with Dilib version V0.6.33. |  |