Foundational (Co)datatypes and (Co)recursion for Higher-Order Logic
Identifieur interne : 000006 ( France/Analysis ); précédent : 000005; suivant : 000007Foundational (Co)datatypes and (Co)recursion for Higher-Order Logic
Auteurs : Julian Biendarra [Allemagne] ; Jasmin Blanchette [Allemagne] ; Aymeric Bouzy [France] ; Martin Desharnais [Allemagne] ; Mathias Fleury [Allemagne] ; Johannes Hölzl [États-Unis] ; Ond Ej Kun Ar [Allemagne] ; Andreas Lochbihler [Suisse] ; Fabian Meier [Suisse] ; Lorenz Panny [Pays-Bas] ; Andrei Popescu [Roumanie] ; Christian Sternagel [Autriche] ; René Thiemann [Autriche] ; Dmitriy Traytel [Suisse]Source :
Abstract
We describe a line of work that started in 2011 towards enriching Isabelle/HOL's language with coinductive datatypes, which allow infinite values, and with a more expressive notion of inductive datatype than previously supported by any system based on higher-order logic. These (co)datatypes are complemented by definitional principles for (co)recursive functions and reasoning principles for (co)induction. In contrast with other systems offering codatatypes, no additional axioms or logic extensions are necessary with our approach.
Url:
DOI: 10.1007/978-3-319-66167-4_1
Affiliations:
- Allemagne, Autriche, France, Pays-Bas, Roumanie, Suisse, États-Unis
- Pennsylvanie
- Pittsburgh
- Société Max-Planck, Université de Pittsburgh
Links toward previous steps (curation, corpus...)
- to stream Hal, to step Corpus: 000290
- to stream Hal, to step Curation: 000290
- to stream Hal, to step Checkpoint: 000007
- to stream Main, to step Merge: 000007
- to stream Main, to step Curation: 000007
- to stream Main, to step Exploration: 000007
- to stream France, to step Extraction: 000006
Links to Exploration step
Hal:hal-01592196Le document en format XML
<record><TEI><teiHeader><fileDesc><titleStmt><title xml:lang="en">Foundational (Co)datatypes and (Co)recursion for Higher-Order Logic</title>
<author><name sortKey="Biendarra, Julian" sort="Biendarra, Julian" uniqKey="Biendarra J" first="Julian" last="Biendarra">Julian Biendarra</name>
<affiliation wicri:level="1"><hal:affiliation type="institution" xml:id="struct-301140" status="VALID"><orgName>Technische Universität München [München]</orgName>
<orgName type="acronym">TUM</orgName>
<desc><address><addrLine>Arcisstraße 21, 80333 München</addrLine>
<country key="DE"></country>
</address>
<ref type="url">http://www.tum.de/</ref>
</desc>
</hal:affiliation>
<country>Allemagne</country>
</affiliation>
</author>
<author><name sortKey="Blanchette, Jasmin" sort="Blanchette, Jasmin" uniqKey="Blanchette J" first="Jasmin" last="Blanchette">Jasmin Blanchette</name>
<affiliation wicri:level="1"><hal:affiliation type="laboratory" xml:id="struct-54489" status="VALID"> <orgName>Max Planck Institut für Informatik</orgName>
<orgName type="acronym">MPII</orgName>
<desc> <address> <addrLine>Max Planck Institut für Informatik Campus E-1 4 66123 Saarbrücken Germany</addrLine>
<country key="DE"></country>
</address>
<ref type="url">http://www.mpi-inf.mpg.de/</ref>
</desc>
<listRelation> <relation active="#struct-300044" type="direct"></relation>
</listRelation>
<tutelles><tutelle active="#struct-300044" type="direct"><org type="institution" xml:id="struct-300044" status="VALID"> <orgName>Max-Planck-Institut</orgName>
<desc> <address> <country key="DE"></country>
</address>
</desc>
</org>
</tutelle>
</tutelles>
</hal:affiliation>
<country>Allemagne</country>
<orgName type="university">Société Max-Planck</orgName>
</affiliation>
</author>
<author><name sortKey="Bouzy, Aymeric" sort="Bouzy, Aymeric" uniqKey="Bouzy A" first="Aymeric" last="Bouzy">Aymeric Bouzy</name>
<affiliation wicri:level="1"><hal:affiliation type="institution" xml:id="struct-507228" status="VALID"> <orgName>InstantJob</orgName>
<desc> <address> <country key="FR"></country>
</address>
<ref type="url">http://www.instantjob.fr/</ref>
</desc>
</hal:affiliation>
<country>France</country>
</affiliation>
</author>
<author><name sortKey="Desharnais, Martin" sort="Desharnais, Martin" uniqKey="Desharnais M" first="Martin" last="Desharnais">Martin Desharnais</name>
<affiliation wicri:level="1"><hal:affiliation type="institution" xml:id="struct-460393" status="VALID"> <orgName>Ludwig Maximilian University [Munich]</orgName>
<orgName type="acronym">LMU</orgName>
<date type="start">2016-07-19</date>
<desc> <address> <addrLine>Professor-Huber-Platz 2, 80539 München, Allemagne</addrLine>
<country key="DE"></country>
</address>
<ref type="url">http://www.jura.uni-muenchen.de/index.html</ref>
</desc>
</hal:affiliation>
<country>Allemagne</country>
</affiliation>
</author>
<author><name sortKey="Fleury, Mathias" sort="Fleury, Mathias" uniqKey="Fleury M" first="Mathias" last="Fleury">Mathias Fleury</name>
<affiliation wicri:level="1"><hal:affiliation type="laboratory" xml:id="struct-54489" status="VALID"> <orgName>Max Planck Institut für Informatik</orgName>
<orgName type="acronym">MPII</orgName>
<desc> <address> <addrLine>Max Planck Institut für Informatik Campus E-1 4 66123 Saarbrücken Germany</addrLine>
<country key="DE"></country>
</address>
<ref type="url">http://www.mpi-inf.mpg.de/</ref>
</desc>
<listRelation> <relation active="#struct-300044" type="direct"></relation>
</listRelation>
<tutelles><tutelle active="#struct-300044" type="direct"><org type="institution" xml:id="struct-300044" status="VALID"> <orgName>Max-Planck-Institut</orgName>
<desc> <address> <country key="DE"></country>
</address>
</desc>
</org>
</tutelle>
</tutelles>
</hal:affiliation>
<country>Allemagne</country>
<orgName type="university">Société Max-Planck</orgName>
</affiliation>
</author>
<author><name sortKey="Holzl, Johannes" sort="Holzl, Johannes" uniqKey="Holzl J" first="Johannes" last="Hölzl">Johannes Hölzl</name>
<affiliation wicri:level="1"><hal:affiliation type="laboratory" xml:id="struct-87723" status="VALID"> <orgName>Computer Science Department - Carnegie Mellon University</orgName>
<desc> <address> <addrLine>Computer Science Department Carnegie Mellon University Pittsburgh, PA</addrLine>
<country key="US"></country>
</address>
<ref type="url">http://www.cs.cmu.edu/</ref>
</desc>
<listRelation> <relation active="#struct-378064" type="direct"></relation>
</listRelation>
<tutelles><tutelle active="#struct-378064" type="direct"><org type="institution" xml:id="struct-378064" status="INCOMING"> <orgName>University of Pittsburgh</orgName>
<desc> <address> <country key="FR"></country>
</address>
</desc>
</org>
</tutelle>
</tutelles>
</hal:affiliation>
<country>États-Unis</country>
<placeName><settlement type="city">Pittsburgh</settlement>
<region type="state">Pennsylvanie</region>
</placeName>
<orgName type="university">Université de Pittsburgh</orgName>
</affiliation>
</author>
<author><name sortKey="Kun Ar, Ond Ej" sort="Kun Ar, Ond Ej" uniqKey="Kun Ar O" first="Ond Ej" last="Kun Ar">Ond Ej Kun Ar</name>
<affiliation wicri:level="1"><hal:affiliation type="institution" xml:id="struct-301140" status="VALID"><orgName>Technische Universität München [München]</orgName>
<orgName type="acronym">TUM</orgName>
<desc><address><addrLine>Arcisstraße 21, 80333 München</addrLine>
<country key="DE"></country>
</address>
<ref type="url">http://www.tum.de/</ref>
</desc>
</hal:affiliation>
<country>Allemagne</country>
</affiliation>
</author>
<author><name sortKey="Lochbihler, Andreas" sort="Lochbihler, Andreas" uniqKey="Lochbihler A" first="Andreas" last="Lochbihler">Andreas Lochbihler</name>
<affiliation wicri:level="1"><hal:affiliation type="institution" xml:id="struct-180925" status="VALID"> <orgName>Eidgenössische Technische Hochschule [Zürich]</orgName>
<orgName type="acronym">ETH Zürich</orgName>
<desc> <address> <addrLine>Hauptgebäude, Rämistrasse 101, 8092 Zürich</addrLine>
<country key="CH"></country>
</address>
<ref type="url">https://www.ethz.ch/</ref>
</desc>
</hal:affiliation>
<country>Suisse</country>
</affiliation>
</author>
<author><name sortKey="Meier, Fabian" sort="Meier, Fabian" uniqKey="Meier F" first="Fabian" last="Meier">Fabian Meier</name>
<affiliation wicri:level="1"><hal:affiliation type="laboratory" xml:id="struct-73149" status="VALID"><orgName>Google Switzerland</orgName>
<desc><address><country key="CH"></country>
</address>
</desc>
<listRelation><relation active="#struct-366136" type="direct"></relation>
</listRelation>
<tutelles><tutelle active="#struct-366136" type="direct"><org type="institution" xml:id="struct-366136" status="VALID"><orgName>Research at Google</orgName>
<desc><address><country key="US"></country>
</address>
<ref type="url">https://research.google.com/</ref>
</desc>
</org>
</tutelle>
</tutelles>
</hal:affiliation>
<country>Suisse</country>
</affiliation>
</author>
<author><name sortKey="Panny, Lorenz" sort="Panny, Lorenz" uniqKey="Panny L" first="Lorenz" last="Panny">Lorenz Panny</name>
<affiliation wicri:level="1"><hal:affiliation type="institution" xml:id="struct-267766" status="VALID"> <orgName>Technische Universiteit Eindhoven</orgName>
<orgName type="acronym">TU/e</orgName>
<desc> <address> <addrLine>Postbus 5135600 MB Eindhoven</addrLine>
<country key="NL"></country>
</address>
<ref type="url">https://www.tue.nl/</ref>
</desc>
</hal:affiliation>
<country>Pays-Bas</country>
</affiliation>
</author>
<author><name sortKey="Popescu, Andrei" sort="Popescu, Andrei" uniqKey="Popescu A" first="Andrei" last="Popescu">Andrei Popescu</name>
<affiliation wicri:level="1"><hal:affiliation type="laboratory" xml:id="struct-104109" status="VALID"> <orgName>"Simion Stoilow" Institute of Mathematics</orgName>
<orgName type="acronym">IMAR</orgName>
<desc> <address> <addrLine>21, Calea Grivitei Street 010702-Bucharest, Sector 1 ROMANIA</addrLine>
<country key="RO"></country>
</address>
<ref type="url">http://www.imar.ro/index.php</ref>
</desc>
<listRelation> <relation active="#struct-300111" type="direct"></relation>
</listRelation>
<tutelles><tutelle active="#struct-300111" type="direct"><org type="institution" xml:id="struct-300111" status="VALID"> <orgName>Romanian Academy of Sciences</orgName>
<desc> <address> <country key="RO"></country>
</address>
</desc>
</org>
</tutelle>
</tutelles>
</hal:affiliation>
<country>Roumanie</country>
</affiliation>
</author>
<author><name sortKey="Sternagel, Christian" sort="Sternagel, Christian" uniqKey="Sternagel C" first="Christian" last="Sternagel">Christian Sternagel</name>
<affiliation wicri:level="1"><hal:affiliation type="department" xml:id="struct-444973" status="VALID"> <orgName>Department of Computer Science [Innsbruck]</orgName>
<desc> <address> <addrLine>Universität InnsbruckTechnikerstraße 21AA - 6020 Innsbruck</addrLine>
<country key="AT"></country>
</address>
<ref type="url">http://informatik.uibk.ac.at</ref>
</desc>
<listRelation> <relation active="#struct-63989" type="direct"></relation>
</listRelation>
<tutelles><tutelle active="#struct-63989" type="direct"><org type="institution" xml:id="struct-63989" status="VALID"> <orgName>University of Innsbruck</orgName>
<desc> <address> <addrLine>Innrain 52, A-6020 Innsbruck</addrLine>
<country key="AT"></country>
</address>
<ref type="url">http://www.uibk.ac.at/</ref>
</desc>
</org>
</tutelle>
</tutelles>
</hal:affiliation>
<country>Autriche</country>
</affiliation>
</author>
<author><name sortKey="Thiemann, Rene" sort="Thiemann, Rene" uniqKey="Thiemann R" first="René" last="Thiemann">René Thiemann</name>
<affiliation wicri:level="1"><hal:affiliation type="department" xml:id="struct-444973" status="VALID"> <orgName>Department of Computer Science [Innsbruck]</orgName>
<desc> <address> <addrLine>Universität InnsbruckTechnikerstraße 21AA - 6020 Innsbruck</addrLine>
<country key="AT"></country>
</address>
<ref type="url">http://informatik.uibk.ac.at</ref>
</desc>
<listRelation> <relation active="#struct-63989" type="direct"></relation>
</listRelation>
<tutelles><tutelle active="#struct-63989" type="direct"><org type="institution" xml:id="struct-63989" status="VALID"> <orgName>University of Innsbruck</orgName>
<desc> <address> <addrLine>Innrain 52, A-6020 Innsbruck</addrLine>
<country key="AT"></country>
</address>
<ref type="url">http://www.uibk.ac.at/</ref>
</desc>
</org>
</tutelle>
</tutelles>
</hal:affiliation>
<country>Autriche</country>
</affiliation>
</author>
<author><name sortKey="Traytel, Dmitriy" sort="Traytel, Dmitriy" uniqKey="Traytel D" first="Dmitriy" last="Traytel">Dmitriy Traytel</name>
<affiliation wicri:level="1"><hal:affiliation type="institution" xml:id="struct-180925" status="VALID"> <orgName>Eidgenössische Technische Hochschule [Zürich]</orgName>
<orgName type="acronym">ETH Zürich</orgName>
<desc> <address> <addrLine>Hauptgebäude, Rämistrasse 101, 8092 Zürich</addrLine>
<country key="CH"></country>
</address>
<ref type="url">https://www.ethz.ch/</ref>
</desc>
</hal:affiliation>
<country>Suisse</country>
</affiliation>
</author>
</titleStmt>
<publicationStmt><idno type="wicri:source">HAL</idno>
<idno type="RBID">Hal:hal-01592196</idno>
<idno type="halId">hal-01592196</idno>
<idno type="halUri">https://hal.inria.fr/hal-01592196</idno>
<idno type="url">https://hal.inria.fr/hal-01592196</idno>
<idno type="doi">10.1007/978-3-319-66167-4_1</idno>
<date when="2017-09">2017-09</date>
<idno type="wicri:Area/Hal/Corpus">000290</idno>
<idno type="wicri:Area/Hal/Curation">000290</idno>
<idno type="wicri:Area/Hal/Checkpoint">000007</idno>
<idno type="wicri:explorRef" wicri:stream="Hal" wicri:step="Checkpoint">000007</idno>
<idno type="wicri:Area/Main/Merge">000007</idno>
<idno type="wicri:Area/Main/Curation">000007</idno>
<idno type="wicri:Area/Main/Exploration">000007</idno>
<idno type="wicri:Area/France/Extraction">000006</idno>
</publicationStmt>
<sourceDesc><biblStruct><analytic><title xml:lang="en">Foundational (Co)datatypes and (Co)recursion for Higher-Order Logic</title>
<author><name sortKey="Biendarra, Julian" sort="Biendarra, Julian" uniqKey="Biendarra J" first="Julian" last="Biendarra">Julian Biendarra</name>
<affiliation wicri:level="1"><hal:affiliation type="institution" xml:id="struct-301140" status="VALID"><orgName>Technische Universität München [München]</orgName>
<orgName type="acronym">TUM</orgName>
<desc><address><addrLine>Arcisstraße 21, 80333 München</addrLine>
<country key="DE"></country>
</address>
<ref type="url">http://www.tum.de/</ref>
</desc>
</hal:affiliation>
<country>Allemagne</country>
</affiliation>
</author>
<author><name sortKey="Blanchette, Jasmin" sort="Blanchette, Jasmin" uniqKey="Blanchette J" first="Jasmin" last="Blanchette">Jasmin Blanchette</name>
<affiliation wicri:level="1"><hal:affiliation type="laboratory" xml:id="struct-54489" status="VALID"> <orgName>Max Planck Institut für Informatik</orgName>
<orgName type="acronym">MPII</orgName>
<desc> <address> <addrLine>Max Planck Institut für Informatik Campus E-1 4 66123 Saarbrücken Germany</addrLine>
<country key="DE"></country>
</address>
<ref type="url">http://www.mpi-inf.mpg.de/</ref>
</desc>
<listRelation> <relation active="#struct-300044" type="direct"></relation>
</listRelation>
<tutelles><tutelle active="#struct-300044" type="direct"><org type="institution" xml:id="struct-300044" status="VALID"> <orgName>Max-Planck-Institut</orgName>
<desc> <address> <country key="DE"></country>
</address>
</desc>
</org>
</tutelle>
</tutelles>
</hal:affiliation>
<country>Allemagne</country>
<orgName type="university">Société Max-Planck</orgName>
</affiliation>
</author>
<author><name sortKey="Bouzy, Aymeric" sort="Bouzy, Aymeric" uniqKey="Bouzy A" first="Aymeric" last="Bouzy">Aymeric Bouzy</name>
<affiliation wicri:level="1"><hal:affiliation type="institution" xml:id="struct-507228" status="VALID"> <orgName>InstantJob</orgName>
<desc> <address> <country key="FR"></country>
</address>
<ref type="url">http://www.instantjob.fr/</ref>
</desc>
</hal:affiliation>
<country>France</country>
</affiliation>
</author>
<author><name sortKey="Desharnais, Martin" sort="Desharnais, Martin" uniqKey="Desharnais M" first="Martin" last="Desharnais">Martin Desharnais</name>
<affiliation wicri:level="1"><hal:affiliation type="institution" xml:id="struct-460393" status="VALID"> <orgName>Ludwig Maximilian University [Munich]</orgName>
<orgName type="acronym">LMU</orgName>
<date type="start">2016-07-19</date>
<desc> <address> <addrLine>Professor-Huber-Platz 2, 80539 München, Allemagne</addrLine>
<country key="DE"></country>
</address>
<ref type="url">http://www.jura.uni-muenchen.de/index.html</ref>
</desc>
</hal:affiliation>
<country>Allemagne</country>
</affiliation>
</author>
<author><name sortKey="Fleury, Mathias" sort="Fleury, Mathias" uniqKey="Fleury M" first="Mathias" last="Fleury">Mathias Fleury</name>
<affiliation wicri:level="1"><hal:affiliation type="laboratory" xml:id="struct-54489" status="VALID"> <orgName>Max Planck Institut für Informatik</orgName>
<orgName type="acronym">MPII</orgName>
<desc> <address> <addrLine>Max Planck Institut für Informatik Campus E-1 4 66123 Saarbrücken Germany</addrLine>
<country key="DE"></country>
</address>
<ref type="url">http://www.mpi-inf.mpg.de/</ref>
</desc>
<listRelation> <relation active="#struct-300044" type="direct"></relation>
</listRelation>
<tutelles><tutelle active="#struct-300044" type="direct"><org type="institution" xml:id="struct-300044" status="VALID"> <orgName>Max-Planck-Institut</orgName>
<desc> <address> <country key="DE"></country>
</address>
</desc>
</org>
</tutelle>
</tutelles>
</hal:affiliation>
<country>Allemagne</country>
<orgName type="university">Société Max-Planck</orgName>
</affiliation>
</author>
<author><name sortKey="Holzl, Johannes" sort="Holzl, Johannes" uniqKey="Holzl J" first="Johannes" last="Hölzl">Johannes Hölzl</name>
<affiliation wicri:level="1"><hal:affiliation type="laboratory" xml:id="struct-87723" status="VALID"> <orgName>Computer Science Department - Carnegie Mellon University</orgName>
<desc> <address> <addrLine>Computer Science Department Carnegie Mellon University Pittsburgh, PA</addrLine>
<country key="US"></country>
</address>
<ref type="url">http://www.cs.cmu.edu/</ref>
</desc>
<listRelation> <relation active="#struct-378064" type="direct"></relation>
</listRelation>
<tutelles><tutelle active="#struct-378064" type="direct"><org type="institution" xml:id="struct-378064" status="INCOMING"> <orgName>University of Pittsburgh</orgName>
<desc> <address> <country key="FR"></country>
</address>
</desc>
</org>
</tutelle>
</tutelles>
</hal:affiliation>
<country>États-Unis</country>
<placeName><settlement type="city">Pittsburgh</settlement>
<region type="state">Pennsylvanie</region>
</placeName>
<orgName type="university">Université de Pittsburgh</orgName>
</affiliation>
</author>
<author><name sortKey="Kun Ar, Ond Ej" sort="Kun Ar, Ond Ej" uniqKey="Kun Ar O" first="Ond Ej" last="Kun Ar">Ond Ej Kun Ar</name>
<affiliation wicri:level="1"><hal:affiliation type="institution" xml:id="struct-301140" status="VALID"><orgName>Technische Universität München [München]</orgName>
<orgName type="acronym">TUM</orgName>
<desc><address><addrLine>Arcisstraße 21, 80333 München</addrLine>
<country key="DE"></country>
</address>
<ref type="url">http://www.tum.de/</ref>
</desc>
</hal:affiliation>
<country>Allemagne</country>
</affiliation>
</author>
<author><name sortKey="Lochbihler, Andreas" sort="Lochbihler, Andreas" uniqKey="Lochbihler A" first="Andreas" last="Lochbihler">Andreas Lochbihler</name>
<affiliation wicri:level="1"><hal:affiliation type="institution" xml:id="struct-180925" status="VALID"> <orgName>Eidgenössische Technische Hochschule [Zürich]</orgName>
<orgName type="acronym">ETH Zürich</orgName>
<desc> <address> <addrLine>Hauptgebäude, Rämistrasse 101, 8092 Zürich</addrLine>
<country key="CH"></country>
</address>
<ref type="url">https://www.ethz.ch/</ref>
</desc>
</hal:affiliation>
<country>Suisse</country>
</affiliation>
</author>
<author><name sortKey="Meier, Fabian" sort="Meier, Fabian" uniqKey="Meier F" first="Fabian" last="Meier">Fabian Meier</name>
<affiliation wicri:level="1"><hal:affiliation type="laboratory" xml:id="struct-73149" status="VALID"><orgName>Google Switzerland</orgName>
<desc><address><country key="CH"></country>
</address>
</desc>
<listRelation><relation active="#struct-366136" type="direct"></relation>
</listRelation>
<tutelles><tutelle active="#struct-366136" type="direct"><org type="institution" xml:id="struct-366136" status="VALID"><orgName>Research at Google</orgName>
<desc><address><country key="US"></country>
</address>
<ref type="url">https://research.google.com/</ref>
</desc>
</org>
</tutelle>
</tutelles>
</hal:affiliation>
<country>Suisse</country>
</affiliation>
</author>
<author><name sortKey="Panny, Lorenz" sort="Panny, Lorenz" uniqKey="Panny L" first="Lorenz" last="Panny">Lorenz Panny</name>
<affiliation wicri:level="1"><hal:affiliation type="institution" xml:id="struct-267766" status="VALID"> <orgName>Technische Universiteit Eindhoven</orgName>
<orgName type="acronym">TU/e</orgName>
<desc> <address> <addrLine>Postbus 5135600 MB Eindhoven</addrLine>
<country key="NL"></country>
</address>
<ref type="url">https://www.tue.nl/</ref>
</desc>
</hal:affiliation>
<country>Pays-Bas</country>
</affiliation>
</author>
<author><name sortKey="Popescu, Andrei" sort="Popescu, Andrei" uniqKey="Popescu A" first="Andrei" last="Popescu">Andrei Popescu</name>
<affiliation wicri:level="1"><hal:affiliation type="laboratory" xml:id="struct-104109" status="VALID"> <orgName>"Simion Stoilow" Institute of Mathematics</orgName>
<orgName type="acronym">IMAR</orgName>
<desc> <address> <addrLine>21, Calea Grivitei Street 010702-Bucharest, Sector 1 ROMANIA</addrLine>
<country key="RO"></country>
</address>
<ref type="url">http://www.imar.ro/index.php</ref>
</desc>
<listRelation> <relation active="#struct-300111" type="direct"></relation>
</listRelation>
<tutelles><tutelle active="#struct-300111" type="direct"><org type="institution" xml:id="struct-300111" status="VALID"> <orgName>Romanian Academy of Sciences</orgName>
<desc> <address> <country key="RO"></country>
</address>
</desc>
</org>
</tutelle>
</tutelles>
</hal:affiliation>
<country>Roumanie</country>
</affiliation>
</author>
<author><name sortKey="Sternagel, Christian" sort="Sternagel, Christian" uniqKey="Sternagel C" first="Christian" last="Sternagel">Christian Sternagel</name>
<affiliation wicri:level="1"><hal:affiliation type="department" xml:id="struct-444973" status="VALID"> <orgName>Department of Computer Science [Innsbruck]</orgName>
<desc> <address> <addrLine>Universität InnsbruckTechnikerstraße 21AA - 6020 Innsbruck</addrLine>
<country key="AT"></country>
</address>
<ref type="url">http://informatik.uibk.ac.at</ref>
</desc>
<listRelation> <relation active="#struct-63989" type="direct"></relation>
</listRelation>
<tutelles><tutelle active="#struct-63989" type="direct"><org type="institution" xml:id="struct-63989" status="VALID"> <orgName>University of Innsbruck</orgName>
<desc> <address> <addrLine>Innrain 52, A-6020 Innsbruck</addrLine>
<country key="AT"></country>
</address>
<ref type="url">http://www.uibk.ac.at/</ref>
</desc>
</org>
</tutelle>
</tutelles>
</hal:affiliation>
<country>Autriche</country>
</affiliation>
</author>
<author><name sortKey="Thiemann, Rene" sort="Thiemann, Rene" uniqKey="Thiemann R" first="René" last="Thiemann">René Thiemann</name>
<affiliation wicri:level="1"><hal:affiliation type="department" xml:id="struct-444973" status="VALID"> <orgName>Department of Computer Science [Innsbruck]</orgName>
<desc> <address> <addrLine>Universität InnsbruckTechnikerstraße 21AA - 6020 Innsbruck</addrLine>
<country key="AT"></country>
</address>
<ref type="url">http://informatik.uibk.ac.at</ref>
</desc>
<listRelation> <relation active="#struct-63989" type="direct"></relation>
</listRelation>
<tutelles><tutelle active="#struct-63989" type="direct"><org type="institution" xml:id="struct-63989" status="VALID"> <orgName>University of Innsbruck</orgName>
<desc> <address> <addrLine>Innrain 52, A-6020 Innsbruck</addrLine>
<country key="AT"></country>
</address>
<ref type="url">http://www.uibk.ac.at/</ref>
</desc>
</org>
</tutelle>
</tutelles>
</hal:affiliation>
<country>Autriche</country>
</affiliation>
</author>
<author><name sortKey="Traytel, Dmitriy" sort="Traytel, Dmitriy" uniqKey="Traytel D" first="Dmitriy" last="Traytel">Dmitriy Traytel</name>
<affiliation wicri:level="1"><hal:affiliation type="institution" xml:id="struct-180925" status="VALID"> <orgName>Eidgenössische Technische Hochschule [Zürich]</orgName>
<orgName type="acronym">ETH Zürich</orgName>
<desc> <address> <addrLine>Hauptgebäude, Rämistrasse 101, 8092 Zürich</addrLine>
<country key="CH"></country>
</address>
<ref type="url">https://www.ethz.ch/</ref>
</desc>
</hal:affiliation>
<country>Suisse</country>
</affiliation>
</author>
</analytic>
<idno type="DOI">10.1007/978-3-319-66167-4_1</idno>
</biblStruct>
</sourceDesc>
</fileDesc>
<profileDesc><textClass></textClass>
</profileDesc>
</teiHeader>
<front><div type="abstract" xml:lang="en">We describe a line of work that started in 2011 towards enriching Isabelle/HOL's language with coinductive datatypes, which allow infinite values, and with a more expressive notion of inductive datatype than previously supported by any system based on higher-order logic. These (co)datatypes are complemented by definitional principles for (co)recursive functions and reasoning principles for (co)induction. In contrast with other systems offering codatatypes, no additional axioms or logic extensions are necessary with our approach.</div>
</front>
</TEI>
<affiliations><list><country><li>Allemagne</li>
<li>Autriche</li>
<li>France</li>
<li>Pays-Bas</li>
<li>Roumanie</li>
<li>Suisse</li>
<li>États-Unis</li>
</country>
<region><li>Pennsylvanie</li>
</region>
<settlement><li>Pittsburgh</li>
</settlement>
<orgName><li>Société Max-Planck</li>
<li>Université de Pittsburgh</li>
</orgName>
</list>
<tree><country name="Allemagne"><noRegion><name sortKey="Biendarra, Julian" sort="Biendarra, Julian" uniqKey="Biendarra J" first="Julian" last="Biendarra">Julian Biendarra</name>
</noRegion>
<name sortKey="Blanchette, Jasmin" sort="Blanchette, Jasmin" uniqKey="Blanchette J" first="Jasmin" last="Blanchette">Jasmin Blanchette</name>
<name sortKey="Desharnais, Martin" sort="Desharnais, Martin" uniqKey="Desharnais M" first="Martin" last="Desharnais">Martin Desharnais</name>
<name sortKey="Fleury, Mathias" sort="Fleury, Mathias" uniqKey="Fleury M" first="Mathias" last="Fleury">Mathias Fleury</name>
<name sortKey="Kun Ar, Ond Ej" sort="Kun Ar, Ond Ej" uniqKey="Kun Ar O" first="Ond Ej" last="Kun Ar">Ond Ej Kun Ar</name>
</country>
<country name="France"><noRegion><name sortKey="Bouzy, Aymeric" sort="Bouzy, Aymeric" uniqKey="Bouzy A" first="Aymeric" last="Bouzy">Aymeric Bouzy</name>
</noRegion>
</country>
<country name="États-Unis"><region name="Pennsylvanie"><name sortKey="Holzl, Johannes" sort="Holzl, Johannes" uniqKey="Holzl J" first="Johannes" last="Hölzl">Johannes Hölzl</name>
</region>
</country>
<country name="Suisse"><noRegion><name sortKey="Lochbihler, Andreas" sort="Lochbihler, Andreas" uniqKey="Lochbihler A" first="Andreas" last="Lochbihler">Andreas Lochbihler</name>
</noRegion>
<name sortKey="Meier, Fabian" sort="Meier, Fabian" uniqKey="Meier F" first="Fabian" last="Meier">Fabian Meier</name>
<name sortKey="Traytel, Dmitriy" sort="Traytel, Dmitriy" uniqKey="Traytel D" first="Dmitriy" last="Traytel">Dmitriy Traytel</name>
</country>
<country name="Pays-Bas"><noRegion><name sortKey="Panny, Lorenz" sort="Panny, Lorenz" uniqKey="Panny L" first="Lorenz" last="Panny">Lorenz Panny</name>
</noRegion>
</country>
<country name="Roumanie"><noRegion><name sortKey="Popescu, Andrei" sort="Popescu, Andrei" uniqKey="Popescu A" first="Andrei" last="Popescu">Andrei Popescu</name>
</noRegion>
</country>
<country name="Autriche"><noRegion><name sortKey="Sternagel, Christian" sort="Sternagel, Christian" uniqKey="Sternagel C" first="Christian" last="Sternagel">Christian Sternagel</name>
</noRegion>
<name sortKey="Thiemann, Rene" sort="Thiemann, Rene" uniqKey="Thiemann R" first="René" last="Thiemann">René Thiemann</name>
</country>
</tree>
</affiliations>
</record>
Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Amérique/explor/PittsburghV1/Data/France/Analysis
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 000006 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/France/Analysis/biblio.hfd -nk 000006 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien |wiki= Wicri/Amérique |area= PittsburghV1 |flux= France |étape= Analysis |type= RBID |clé= Hal:hal-01592196 |texte= Foundational (Co)datatypes and (Co)recursion for Higher-Order Logic }}
This area was generated with Dilib version V0.6.38. |