| HAL-Inria | Publications, software ... of Inria's scientists |
Conference papers
Foundational (Co)datatypes and (Co)recursion for Higher-Order Logic
Julian Biendarra
1
Jasmin Blanchette
2, 3, 4
Aymeric Bouzy
5
Martin Desharnais
6
Mathias Fleury
2, 3
Johannes Hölzl
7
Ondřej Kunčar
1
Andreas Lochbihler
8
Fabian Meier
9
Lorenz Panny
10
Andrei Popescu
11, 12
Christian Sternagel
13
René Thiemann
13
Dmitriy Traytel
8
3
VERIDIS - Modeling and Verification of Distributed Algorithms and Systems
MPII - Max-Planck-Institut für Informatik, Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
Julian Biendarra 1
Author
Jasmin Christian Blanchette 2, 3, 4
Author
Aymeric Bouzy 5
Author
Martin Desharnais 6
Author
Mathias Fleury 2, 3
Author IdHAL : mathias-fleury ORCID : https://orcid.org/0000-0002-1705-3083
Johannes Hölzl 7
Author
Ondřej Kunčar 1
Author
Andreas Lochbihler 8
Author
Fabian Meier 9
Author
Lorenz Panny 10
Author
Andrei Popescu 11, 12
Author IdHAL : andrei-popescu
Christian Christian Sternagel 13
Author
René Thiemann 13
Author
Dmitriy Traytel 8
Author
1
TUM - Technische Universität München [München] (Arcisstraße 21, 80333 München - Germany)
2
MPII - Max-Planck-Institut für Informatik (Campus E-1 4, 66123 Saarbrücken, Germany - Germany)
- Max-Planck-Gesellschaft (Jägerstrasse, 10-11, D-10117 Berlin - Germany)
3
VERIDIS - Modeling and Verification of Distributed Algorithms and Systems (France)
- MPII - Max-Planck-Institut für Informatik (Campus E-1 4, 66123 Saarbrücken, Germany - Germany)
- Max-Planck-Gesellschaft (Jägerstrasse, 10-11, D-10117 Berlin - Germany)
- Inria Nancy - Grand Est (615 rue du Jardin Botanique 54600 Villers-lès-Nancy - France)
- Inria - Institut National de Recherche en Informatique et en Automatique (Domaine de Voluceau Rocquencourt - BP 105 78153 Le Chesnay Cedex - France)
- LORIA - FM - Department of Formal Methods (France)
- LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications (Campus Scientifique BP 239 54506 Vandoeuvre-lès-Nancy Cedex - France)
- Inria - Institut National de Recherche en Informatique et en Automatique (Domaine de Voluceau Rocquencourt - BP 105 78153 Le Chesnay Cedex - France)
- UL - Université de Lorraine (34 cours Léopold - CS 25233 - 54052 Nancy cedex - France)
- CNRS - Centre National de la Recherche Scientifique : UMR7503 (France)
- LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications (Campus Scientifique BP 239 54506 Vandoeuvre-lès-Nancy Cedex - France)
4
VU - Vrije Universiteit Amsterdam [Amsterdam] (De Boelelaan 1105 1081 HV Amsterdam - Netherlands)
5
InstantJob (France)
6
LMU - Ludwig Maximilian University [Munich] (Professor-Huber-Platz 2, 80539 München, Allemagne - Germany)
7
Computer Science Department - Carnegie Mellon University (Computer Science Department Carnegie Mellon University Pittsburgh, PA - United States)
- PITT - University of Pittsburgh (4200 Fifth Avenue Pittsburgh, PA 15260 - United States)
- Pennsylvania Commonwealth System of Higher Education (PCSHE) (United States)
8
ETH Zürich - Eidgenössische Technische Hochschule - Swiss Federal Institute of Technology in Zürich [Zürich] (Hauptgebäude,
Rämistrasse 101,
8092 Zürich - Switzerland)
10
TU/e - Technische Universiteit Eindhoven (Postbus 513
5600 MB Eindhoven - Netherlands)
11
IMAR - "Simion Stoilow" Institute of Mathematics (21, Calea Grivitei Street 010702-Bucharest, Sector 1 ROMANIA - Romania)
- Romanian Academy of Sciences (Romania)
12
Middlesex University [London] (Hendon Campus, The Burroughs, Hendon;NW4 4BT;London - United Kingdom)
13
Department of Computer Science [Innsbruck] (Universität Innsbruck
Technikerstraße 21A
A - 6020 Innsbruck - Austria)
- University of Innsbruck (Innrain 52, A-6020 Innsbruck - Austria)
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.
Document type :
Conference papers
Complete list of metadatas
https://hal.inria.fr/hal-01592196
Contributor : Stephan Merz <>
Submitted on : Wednesday, September 27, 2017 - 3:12:59 PM
Last modification on : Wednesday, October 14, 2020 - 4:01:44 AM
Long-term archiving on: : Thursday, December 28, 2017 - 12:42:34 PM
Contributor : Stephan Merz <>
Submitted on : Wednesday, September 27, 2017 - 3:12:59 PM
Last modification on : Wednesday, October 14, 2020 - 4:01:44 AM
Long-term archiving on: : Thursday, December 28, 2017 - 12:42:34 PM
File
BiendarraBlanchetteEtAl-FroCos...
Files produced by the author(s)
Identifiers
- HAL Id : hal-01592196, version 1
- DOI : 10.1007/978-3-319-66167-4_1
Collections
CNRS | LORIA | LORIA-FM | UNIV-LORRAINE | INRIA
Citation
Julian Biendarra, Jasmin Blanchette, Aymeric Bouzy, Martin Desharnais, Mathias Fleury, et al.. Foundational (Co)datatypes and (Co)recursion for Higher-Order Logic. Frontiers of Combining Systems, 11th International Symposium, Sep 2017, Brasilia, Brazil. pp.3-21, ⟨10.1007/978-3-319-66167-4_1⟩. ⟨hal-01592196⟩
Metrics
Record views
697
Files downloads