Opendata, web and dolomites

CoqHoTT SIGNED

Coq for Homotopy Type Theory

Total Cost €

0

EC-Contrib. €

0

Partnership

0

Views

0

Project "CoqHoTT" data sheet

The following table provides information about the project.

Coordinator
INSTITUT NATIONAL DE RECHERCHE ENINFORMATIQUE ET AUTOMATIQUE 

Organization address
address: DOMAINE DE VOLUCEAU ROCQUENCOURT
city: LE CHESNAY CEDEX
postcode: 78153
website: www.inria.fr

contact info
title: n.a.
name: n.a.
surname: n.a.
function: n.a.
email: n.a.
telephone: n.a.
fax: n.a.

 Coordinator Country France [FR]
 Project website http://coqhott.gforge.inria.fr/
 Total cost 1˙498˙290 €
 EC max contribution 1˙498˙290 € (100%)
 Programme 1. H2020-EU.1.1. (EXCELLENT SCIENCE - European Research Council (ERC))
 Code Call ERC-2014-STG
 Funding Scheme ERC-STG
 Starting year 2015
 Duration (year-month-day) from 2015-06-01   to  2020-05-31

 Partnership

Take a look of project's partnership.

# participants  country  role  EC contrib. [€] 
1    INSTITUT NATIONAL DE RECHERCHE ENINFORMATIQUE ET AUTOMATIQUE FR (LE CHESNAY CEDEX) coordinator 1˙498˙290.00

Map

 Project objective

Every year, software bugs cost hundreds of millions of euros to companies and administrations. Hence, software quality is a prevalent notion and interactive theorem provers based on type theory have shown their efficiency to prove correctness of important pieces of software like the C compiler of the CompCert project. One main interest of such theorem provers is the ability to extract directly the code from the proof. Unfortunately, their democratization suffers from a major drawback, the mismatch between equality in mathematics and in type theory. Thus, significant Coq developments have only been done by virtuosos playing with advanced concepts of computer science and mathematics. Recently, an extension of type theory with homotopical concepts such as univalence is gaining traction because it allows for the first time to marry together expected principles of equality. But the univalence principle has been treated so far as a new axiom which breaks one fundamental property of mechanized proofs: the ability to compute with programs that make use of this axiom. The main goal of the CoqHoTT project is to provide a new generation of proof assistants with a computational version of univalence and use them as a base to implement effective logical model transformation so that the power of the internal logic of the proof assistant needed to prove the correctness of a program can be decided and changed at compile time—according to a trade-off between efficiency and logical expressivity. Our approach is based on a radically new compilation phase technique into a core type theory to modularize the difficulty of finding a decidable type checking algorithm for homotopy type theory. The impact of the CoqHoTT project will be very strong. Even if Coq is already a success, this project will promote it as a major proof assistant, for both computer scientists and mathematicians. CoqHoTT will become an essential tool for program certification and formalization of mathematics.

 Publications

year authors and title journal last update
List of publications.
2019 Benedikt Ahrens, Ralph Matthes, Anders Mörtberg
From Signatures to Monads in UniMath
published pages: 285-318, ISSN: 0168-7433, DOI: 10.1007/s10817-018-9474-4
Journal of Automated Reasoning 63/2 2020-04-23
2018 M. Anel, G. Biedermann, E. Finster, A. Joyal
Goodwillie\'s calculus of functors and higher topos theory
published pages: 1100-1132, ISSN: 1753-8416, DOI: 10.1112/topo.12082
Journal of Topology 11/4 2020-04-23
2019 Pierre-Marie Pédrot, Nicolas Tabareau, Hans Jacob Fehrmann, Éric Tanter
A reasonably exceptional type theory
published pages: 1-29, ISSN: 2475-1421, DOI: 10.1145/3341712
Proceedings of the ACM on Programming Languages 3/ICFP 2020-04-23
2018 Nicolas Tabareau, Éric Tanter, Matthieu Sozeau
Equivalences for free: univalent parametricity for effective transport
published pages: 1-29, ISSN: 2475-1421, DOI: 10.1145/3236787
Proceedings of the ACM on Programming Languages 2/ICFP 2020-04-23
2018 Martin Elsman, Troels Henriksen, Danil Annenkov, Cosmin E. Oancea
Static interpretation of higher-order modules in Futhark: functional GPU programming in the large
published pages: 1-30, ISSN: 2475-1421, DOI: 10.1145/3236792
Proceedings of the ACM on Programming Languages 2/ICFP 2020-04-23
2020 Benedikt Ahrens, André Hirschowitz, Ambroise Lafont, Marco Maggesi
Reduction monads and their signatures
published pages: 1-29, ISSN: 2475-1421, DOI: 10.1145/3371099
Proceedings of the ACM on Programming Languages 4/POPL 2020-04-23
2019 Gaëtan Gilbert, Jesper Cockx, Matthieu Sozeau, Nicolas Tabareau
Definitional proof-irrelevance without K
published pages: 1-28, ISSN: 2475-1421, DOI: 10.1145/3290316
Proceedings of the ACM on Programming Languages 3/POPL 2020-04-23
2019 Matthieu Sozeau, Cyprien Mangin
Equations reloaded: high-level dependently-typed functional programming and proving in Coq
published pages: 1-29, ISSN: 2475-1421, DOI: 10.1145/3341690
Proceedings of the ACM on Programming Languages 3/ICFP 2020-04-23
2016 Kevin Quirin and Nicolas Tabareau
Lawvere-Tierney sheafification in Homotopy Type Theory
published pages: , ISSN: 1972-5787, DOI: 10.6092/issn.1972-5787/6232
Journal of Formalized Reasoning 2020-04-23
2017 Ahrens, Benedikt; Lumsdaine, Peter LeFanu
Displayed Categories
published pages: , ISSN: , DOI: 10.4230/LIPIcs.FSCD.2017.5
https://hal.inria.fr/hal-01584770 7 2020-04-23
2017 Ahrens, Benedikt; Lumsdaine, Peter LeFanu; Voevodsky, Vladimir
Categorical Structures for Type Theory in Univalent Foundations
published pages: , ISSN: , DOI: 10.4230/LIPIcs.CSL.2017.8
26th EACSL Annual Conference on Computer Science Logic (CSL 2017) 6 2020-04-23
2018 PIERRE-ÉVARISTE DAGAND, NICOLAS TABAREAU, ÉRIC TANTER
Foundations of dependent interoperability
published pages: , ISSN: 0956-7968, DOI: 10.1017/S0956796818000011
Journal of Functional Programming 28 2020-04-23

Are you the coordinator (or a participant) of this project? Plaese send me more information about the "COQHOTT" project.

For instance: the website url (it has not provided by EU-opendata yet), the logo, a more detailed description of the project (in plain text as a rtf file or a word file), some pictures (as picture files, not embedded into any word file), twitter account, linkedin page, etc.

Send me an  email (fabio@fabiodisconzi.com) and I put them in your project's page as son as possible.

Thanks. And then put a link of this page into your project's website.

The information about "COQHOTT" are provided by the European Opendata Portal: CORDIS opendata.

More projects from the same programme (H2020-EU.1.1.)

PROGRESS (2019)

The Enemy of the Good: Towards a Theory of Moral Progress

Read More  

KEYNESGROWTH (2020)

Economic Fluctuations, Productivity Growth and Stabilization Policies: A Keynesian Growth Perspective

Read More  

Photopharm (2020)

Photopharmacology: From Academia toward the Clinic.

Read More