Second Order Isomorphic Types: A Proof Theoretic Study on Second Order λ-Calculus with Surjective Pairing and Terminal Object
Identifieur interne : 002363 ( Istex/Corpus ); précédent : 002362; suivant : 002364Second Order Isomorphic Types: A Proof Theoretic Study on Second Order λ-Calculus with Surjective Pairing and Terminal Object
Auteurs : R. DicosmoSource :
- Information and Computation [ 0890-5401 ] ; 1995.
Abstract
Abstract: We investigate invertible terms and isomorphic types in the second order lambda calculus extended with surjective pairs and terminal (or Unit) type. These two topics are closely related: on one side, the study of invertibility is a necessary tool for the characterization of isomorphic types; on the other hand, we need the notion of isomorphic types to study the typed invertible terms. The result of our investigation is twofold: we give a constructive characterization of the invertible terms, extending previous work by Dezani and Bruce-Longo, and a decidable equational theory of the isomorphisms of types which hold in all models of the calculus, which is a conservative extension to the second order case of the results previously achieved for the case of first order typed calculi. Via the Curry-Howard correspondence, this work also provides a decision procedure for strong equivalence of formulae in second order intuitionistic positive propositional logic, that is suitable to search equivalent proofs in automated deduction systems.
Url:
DOI: 10.1006/inco.1995.1085
Links to Exploration step
ISTEX:988356788C8947A113E5083C19A074DD6F667BECLe document en format XML
<record><TEI wicri:istexFullTextTei="biblStruct"><teiHeader><fileDesc><titleStmt><title xml:lang="en">Second Order Isomorphic Types: A Proof Theoretic Study on Second Order λ-Calculus with Surjective Pairing and Terminal Object</title><author><name sortKey="Dicosmo, R" sort="Dicosmo, R" uniqKey="Dicosmo R" first="R." last="Dicosmo">R. Dicosmo</name><affiliation><mods:affiliation>Ecole Normale Super, Liens, CNRS, 45 Rue Ulm, F 75005 Paris, France; Corso Italia, Dipartimento Informat, I 56100 Pisa, Italy and Cornell Univ, Dept Comp Sci, Ithaca, NY 14853, USA</mods:affiliation></affiliation></author></titleStmt><publicationStmt><idno type="wicri:source">ISTEX</idno><idno type="RBID">ISTEX:988356788C8947A113E5083C19A074DD6F667BEC</idno><date when="1995" year="1995">1995</date><idno type="doi">10.1006/inco.1995.1085</idno><idno type="url">https://api.istex.fr/ark:/67375/6H6-GRJ6JHJT-F/fulltext.pdf</idno><idno type="wicri:Area/Istex/Corpus">002363</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">002363</idno></publicationStmt><sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="en">Second Order Isomorphic Types: A Proof Theoretic Study on Second Order λ-Calculus with Surjective Pairing and Terminal Object</title><author><name sortKey="Dicosmo, R" sort="Dicosmo, R" uniqKey="Dicosmo R" first="R." last="Dicosmo">R. Dicosmo</name><affiliation><mods:affiliation>Ecole Normale Super, Liens, CNRS, 45 Rue Ulm, F 75005 Paris, France; Corso Italia, Dipartimento Informat, I 56100 Pisa, Italy and Cornell Univ, Dept Comp Sci, Ithaca, NY 14853, USA</mods:affiliation></affiliation></author></analytic><monogr></monogr><series><title level="j">Information and Computation</title><title level="j" type="abbrev">YINCO</title><idno type="ISSN">0890-5401</idno><imprint><publisher>ELSEVIER</publisher><date type="published" when="1995">1995</date><biblScope unit="volume">119</biblScope><biblScope unit="issue">2</biblScope><biblScope unit="page" from="176">176</biblScope><biblScope unit="page" to="201">201</biblScope></imprint><idno type="ISSN">0890-5401</idno></series></biblStruct></sourceDesc><seriesStmt><idno type="ISSN">0890-5401</idno></seriesStmt></fileDesc><profileDesc><textClass></textClass><langUsage><language ident="en">en</language></langUsage></profileDesc></teiHeader><front><div type="abstract" xml:lang="en">Abstract: We investigate invertible terms and isomorphic types in the second order lambda calculus extended with surjective pairs and terminal (or Unit) type. These two topics are closely related: on one side, the study of invertibility is a necessary tool for the characterization of isomorphic types; on the other hand, we need the notion of isomorphic types to study the typed invertible terms. The result of our investigation is twofold: we give a constructive characterization of the invertible terms, extending previous work by Dezani and Bruce-Longo, and a decidable equational theory of the isomorphisms of types which hold in all models of the calculus, which is a conservative extension to the second order case of the results previously achieved for the case of first order typed calculi. Via the Curry-Howard correspondence, this work also provides a decision procedure for strong equivalence of formulae in second order intuitionistic positive propositional logic, that is suitable to search equivalent proofs in automated deduction systems.</div></front></TEI><istex><corpusName>elsevier</corpusName><author><json:item><name>R. Dicosmo</name><affiliations><json:string>Ecole Normale Super, Liens, CNRS, 45 Rue Ulm, F 75005 Paris, France; Corso Italia, Dipartimento Informat, I 56100 Pisa, Italy and Cornell Univ, Dept Comp Sci, Ithaca, NY 14853, USA</json:string></affiliations></json:item></author><arkIstex>ark:/67375/6H6-GRJ6JHJT-F</arkIstex><language><json:string>eng</json:string></language><originalGenre><json:string>Full-length article</json:string></originalGenre><abstract>Abstract: We investigate invertible terms and isomorphic types in the second order lambda calculus extended with surjective pairs and terminal (or Unit) type. These two topics are closely related: on one side, the study of invertibility is a necessary tool for the characterization of isomorphic types; on the other hand, we need the notion of isomorphic types to study the typed invertible terms. The result of our investigation is twofold: we give a constructive characterization of the invertible terms, extending previous work by Dezani and Bruce-Longo, and a decidable equational theory of the isomorphisms of types which hold in all models of the calculus, which is a conservative extension to the second order case of the results previously achieved for the case of first order typed calculi. Via the Curry-Howard correspondence, this work also provides a decision procedure for strong equivalence of formulae in second order intuitionistic positive propositional logic, that is suitable to search equivalent proofs in automated deduction systems.</abstract><qualityIndicators><score>3.982</score><pdfWordCount>0</pdfWordCount><pdfCharCount>0</pdfCharCount><pdfVersion>1.2</pdfVersion><pdfPageCount>26</pdfPageCount><pdfPageSize>568 x 814 pts</pdfPageSize><refBibsNative>false</refBibsNative><abstractWordCount>161</abstractWordCount><abstractCharCount>1054</abstractCharCount><keywordCount>0</keywordCount></qualityIndicators><title>Second Order Isomorphic Types: A Proof Theoretic Study on Second Order λ-Calculus with Surjective Pairing and Terminal Object</title><pii><json:string>S0890-5401(85)71085-1</json:string></pii><genre><json:string>research-article</json:string></genre><host><title>Information and Computation</title><language><json:string>unknown</json:string></language><publicationDate>1995</publicationDate><issn><json:string>0890-5401</json:string></issn><pii><json:string>S0890-5401(00)X0101-0</json:string></pii><volume>119</volume><issue>2</issue><pages><first>176</first><last>201</last></pages><genre><json:string>journal</json:string></genre></host><namedEntities><unitex><date><json:string>1995</json:string></date><geogName></geogName><orgName></orgName><orgName_funder></orgName_funder><orgName_provider></orgName_provider><persName></persName><placeName></placeName><ref_url></ref_url><ref_bibl></ref_bibl><bibl></bibl></unitex></namedEntities><ark><json:string>ark:/67375/6H6-GRJ6JHJT-F</json:string></ark><categories><wos><json:string>1 - science</json:string><json:string>2 - mathematics, applied</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 - Computational Theory and Mathematics</json:string><json:string>1 - Physical Sciences</json:string><json:string>2 - Computer Science</json:string><json:string>3 - Computer Science Applications</json:string><json:string>1 - Physical Sciences</json:string><json:string>2 - Computer Science</json:string><json:string>3 - Information Systems</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 appliquees, technologies et medecines</json:string><json:string>2 - sciences exactes et technologie</json:string><json:string>3 - sciences et techniques communes</json:string><json:string>4 - mathematiques</json:string></inist></categories><publicationDate>1995</publicationDate><copyrightDate>1995</copyrightDate><doi><json:string>10.1006/inco.1995.1085</json:string></doi><id>988356788C8947A113E5083C19A074DD6F667BEC</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-GRJ6JHJT-F/fulltext.pdf</uri></json:item><json:item><extension>ocr</extension><original>false</original><mimetype>text/ocr</mimetype><uri>https://api.istex.fr/ark:/67375/6H6-GRJ6JHJT-F/fulltext.ocr</uri></json:item><json:item><extension>zip</extension><original>false</original><mimetype>application/zip</mimetype><uri>https://api.istex.fr/ark:/67375/6H6-GRJ6JHJT-F/bundle.zip</uri></json:item><istex:fulltextTEI uri="https://api.istex.fr/ark:/67375/6H6-GRJ6JHJT-F/fulltext.tei"><teiHeader><fileDesc><titleStmt><title level="a" type="main" xml:lang="en">Second Order Isomorphic Types: A Proof Theoretic Study on Second Order λ-Calculus with Surjective Pairing and Terminal Object</title></titleStmt><publicationStmt><authority>ISTEX</authority><publisher scheme="https://scientific-publisher.data.istex.fr">ELSEVIER</publisher><availability><licence><p>©1995 Academic Press</p></licence><p scheme="https://loaded-corpus.data.istex.fr/ark:/67375/XBH-HKKZVM7B-M">elsevier</p></availability><date>1995</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><note type="content">Section title: Regular Article</note></notesStmt><sourceDesc><biblStruct type="inbook"><analytic><title level="a" type="main" xml:lang="en">Second Order Isomorphic Types: A Proof Theoretic Study on Second Order λ-Calculus with Surjective Pairing and Terminal Object</title><author xml:id="author-0000"><persName><forename type="first">R.</forename><surname>Dicosmo</surname></persName><affiliation>Ecole Normale Super, Liens, CNRS, 45 Rue Ulm, F 75005 Paris, France; Corso Italia, Dipartimento Informat, I 56100 Pisa, Italy and Cornell Univ, Dept Comp Sci, Ithaca, NY 14853, USA</affiliation></author><idno type="istex">988356788C8947A113E5083C19A074DD6F667BEC</idno><idno type="ark">ark:/67375/6H6-GRJ6JHJT-F</idno><idno type="DOI">10.1006/inco.1995.1085</idno><idno type="PII">S0890-5401(85)71085-1</idno></analytic><monogr><title level="j">Information and Computation</title><title level="j" type="abbrev">YINCO</title><idno type="pISSN">0890-5401</idno><idno type="PII">S0890-5401(00)X0101-0</idno><imprint><publisher>ELSEVIER</publisher><date type="published" when="1995"></date><biblScope unit="volume">119</biblScope><biblScope unit="issue">2</biblScope><biblScope unit="page" from="176">176</biblScope><biblScope unit="page" to="201">201</biblScope></imprint></monogr></biblStruct></sourceDesc></fileDesc><profileDesc><creation><date>1995</date></creation><langUsage><language ident="en">en</language></langUsage><abstract xml:lang="en"><p>Abstract: We investigate invertible terms and isomorphic types in the second order lambda calculus extended with surjective pairs and terminal (or Unit) type. These two topics are closely related: on one side, the study of invertibility is a necessary tool for the characterization of isomorphic types; on the other hand, we need the notion of isomorphic types to study the typed invertible terms. The result of our investigation is twofold: we give a constructive characterization of the invertible terms, extending previous work by Dezani and Bruce-Longo, and a decidable equational theory of the isomorphisms of types which hold in all models of the calculus, which is a conservative extension to the second order case of the results previously achieved for the case of first order typed calculi. Via the Curry-Howard correspondence, this work also provides a decision procedure for strong equivalence of formulae in second order intuitionistic positive propositional logic, that is suitable to search equivalent proofs in automated deduction systems.</p></abstract></profileDesc><revisionDesc><change when="1995">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-GRJ6JHJT-F/fulltext.txt</uri></json:item></fulltext><metadata><istex:metadataXml wicri:clean="Elsevier converted-article found"><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" xml:lang="en"><item-info><jid>YINCO</jid><aid>71085</aid><ce:pii>S0890-5401(85)71085-1</ce:pii><ce:doi>10.1006/inco.1995.1085</ce:doi><ce:copyright type="full-transfer" year="1995">Academic Press</ce:copyright></item-info><head><ce:dochead><ce:textfn>Regular Article</ce:textfn></ce:dochead><ce:title>Second Order Isomorphic Types: A Proof Theoretic Study on Second Order λ-Calculus with Surjective Pairing and Terminal Object</ce:title><ce:author-group><ce:author><ce:surname>Dicosmo</ce:surname><ce:given-name>R.</ce:given-name></ce:author><ce:affiliation><ce:textfn>Ecole Normale Super, Liens, CNRS, 45 Rue Ulm, F 75005 Paris, France; Corso Italia, Dipartimento Informat, I 56100 Pisa, Italy and Cornell Univ, Dept Comp Sci, Ithaca, NY 14853, USA</ce:textfn></ce:affiliation></ce:author-group><ce:abstract><ce:section-title>Abstract</ce:section-title><ce:abstract-sec><ce:simple-para>We investigate invertible terms and isomorphic types in the second order lambda calculus extended with surjective pairs and terminal (or <ce:italic>Unit</ce:italic>) type. These two topics are closely related: on one side, the study of invertibility is a necessary tool for the characterization of isomorphic types; on the other hand, we need the notion of isomorphic types to study the typed invertible terms. The result of our investigation is twofold: we give a constructive characterization of the invertible terms, extending previous work by Dezani and Bruce-Longo, and a decidable equational theory of the isomorphisms of types which hold in all models of the calculus, which is a conservative extension to the second order case of the results previously achieved for the case of first order typed calculi. Via the Curry-Howard correspondence, this work also provides a decision procedure for <ce:italic>strong equivalence</ce:italic> of formulae in second order intuitionistic positive propositional logic, that is suitable to search equivalent proofs in automated deduction systems.</ce:simple-para></ce:abstract-sec></ce:abstract></head></converted-article></istex:document></istex:metadataXml><mods version="3.6"><titleInfo lang="en"><title>Second Order Isomorphic Types: A Proof Theoretic Study on Second Order λ-Calculus with Surjective Pairing and Terminal Object</title></titleInfo><titleInfo type="alternative" lang="en" contentType="CDATA"><title>Second Order Isomorphic Types: A Proof Theoretic Study on Second Order λ-Calculus with Surjective Pairing and Terminal Object</title></titleInfo><name type="personal"><namePart type="given">R.</namePart><namePart type="family">Dicosmo</namePart><affiliation>Ecole Normale Super, Liens, CNRS, 45 Rue Ulm, F 75005 Paris, France; Corso Italia, Dipartimento Informat, I 56100 Pisa, Italy and Cornell Univ, Dept Comp Sci, Ithaca, NY 14853, USA</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">1995</dateIssued><copyrightDate encoding="w3cdtf">1995</copyrightDate></originInfo><language><languageTerm type="code" authority="iso639-2b">eng</languageTerm><languageTerm type="code" authority="rfc3066">en</languageTerm></language><abstract lang="en">Abstract: We investigate invertible terms and isomorphic types in the second order lambda calculus extended with surjective pairs and terminal (or Unit) type. These two topics are closely related: on one side, the study of invertibility is a necessary tool for the characterization of isomorphic types; on the other hand, we need the notion of isomorphic types to study the typed invertible terms. The result of our investigation is twofold: we give a constructive characterization of the invertible terms, extending previous work by Dezani and Bruce-Longo, and a decidable equational theory of the isomorphisms of types which hold in all models of the calculus, which is a conservative extension to the second order case of the results previously achieved for the case of first order typed calculi. Via the Curry-Howard correspondence, this work also provides a decision procedure for strong equivalence of formulae in second order intuitionistic positive propositional logic, that is suitable to search equivalent proofs in automated deduction systems.</abstract><note type="content">Section title: Regular Article</note><relatedItem type="host"><titleInfo><title>Information and Computation</title></titleInfo><titleInfo type="abbreviated"><title>YINCO</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">1995</dateIssued></originInfo><identifier type="ISSN">0890-5401</identifier><identifier type="PII">S0890-5401(00)X0101-0</identifier><part><date>1995</date><detail type="volume"><number>119</number><caption>vol.</caption></detail><detail type="issue"><number>2</number><caption>no.</caption></detail><extent unit="issue-pages"><start>137</start><end>294</end></extent><extent unit="pages"><start>176</start><end>201</end></extent></part></relatedItem><identifier type="istex">988356788C8947A113E5083C19A074DD6F667BEC</identifier><identifier type="ark">ark:/67375/6H6-GRJ6JHJT-F</identifier><identifier type="DOI">10.1006/inco.1995.1085</identifier><identifier type="PII">S0890-5401(85)71085-1</identifier><accessCondition type="use and reproduction" contentType="copyright">©1995 Academic Press</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>Academic Press, ©1995</recordOrigin></recordInfo></mods><json:item><extension>json</extension><original>false</original><mimetype>application/json</mimetype><uri>https://api.istex.fr/ark:/67375/6H6-GRJ6JHJT-F/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 002363 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Istex/Corpus/biblio.hfd -nk 002363 | 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:988356788C8947A113E5083C19A074DD6F667BEC
|texte= Second Order Isomorphic Types: A Proof Theoretic Study on Second Order λ-Calculus with Surjective Pairing and Terminal Object
}}
| This area was generated with Dilib version V0.6.33. |  |