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. | ![]() |