Back to Search Start Over

Correct and Complete Type Checking and Certified Erasure for Coq, in Coq

Authors :
Sozeau, Matthieu
Forster, Yannick
Lennon-Bertrand, Meven
Nielsen, Jakob
Tabareau, Nicolas
Winterhalter, Théo
Laboratoire des Sciences du Numérique de Nantes (LS2N)
Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-IMT Atlantique (IMT Atlantique)
Institut Mines-Télécom [Paris] (IMT)-Institut Mines-Télécom [Paris] (IMT)-École Centrale de Nantes (Nantes Univ - ECN)
Nantes Université (Nantes Univ)-Nantes Université (Nantes Univ)-Nantes université - UFR des Sciences et des Techniques (Nantes univ - UFR ST)
Nantes Université - pôle Sciences et technologie
Nantes Université (Nantes Univ)-Nantes Université (Nantes Univ)-Nantes Université - pôle Sciences et technologie
Nantes Université (Nantes Univ)
Gallinette : vers une nouvelle génération d'assistant à la preuve (GALLINETTE)
Inria Rennes – Bretagne Atlantique
Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire des Sciences du Numérique de Nantes (LS2N)
Nantes Université (Nantes Univ)-Centre National de la Recherche Scientifique (CNRS)-IMT Atlantique (IMT Atlantique)
University of Cambridge [UK] (CAM)
Aarhus University [Aarhus]
Département Automatique, Productique et Informatique (IMT Atlantique - DAPI)
IMT Atlantique (IMT Atlantique)
Institut Mines-Télécom [Paris] (IMT)-Institut Mines-Télécom [Paris] (IMT)
Deduction modulo, interopérabilité et démonstration automatique (DEDUCTEAM)
Inria Saclay - Ile de France
Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Méthodes Formelles (LMF)
Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay)
Marie-Curie Grant Agreement No. 101024493.
Publication Year :
2023
Publisher :
HAL CCSD, 2023.

Subjects

Subjects :
certification
proof assistants
type checker
Coq
[INFO]Computer Science [cs]

Details

Language :
English
Database :
OpenAIRE
Accession number :
edsair.od.......165..9c9645ac79da0b731d3141a224bb241e

Tools

Authors Abstract Subjects Details