Coq (logiciel)

Coq est un assistant de preuve utilisant le langage Gallina, développé par l'équipe PI.R2 de l’Inria au sein du laboratoire PPS du CNRS et en partenariat avec l'École polytechnique, le CNAM, l'Université Paris Diderot et l'Université Paris-Sud (et antérieurement l'École normale supérieure de Lyon). Le nom du logiciel (initialement CoC) est particulièrement adéquat car : il est français ; il est fondé sur le calcul des constructions (CoC abrégé en anglais) introduit par Thierry Coquand. Dans la même veine, son langage est Gallina et Coq possède un wiki dédié, baptisé Cocorico!. En 2013, Coq a été récompensé du Programming Languages Software Award par l'ACM SIGPLAN. Coq a reçu en 2022 le premier prix science ouverte du logiciel libre de la recherche dans la catégorie « scientifique et technique ». Historique du projet Au début des années 80, Gérard Huet lance un proj

À propos de ce résultat

Cette page est générée automatiquement et peut contenir des informations qui ne sont pas correctes, complètes, à jour ou pertinentes par rapport à votre recherche. Il en va de même pour toutes les autres pages de ce site. Veillez à vérifier les informations auprès des sources officielles de l'EPFL.

Publications associées

Chargement

Personnes associées

Chargement

Unités associées

Chargement

Concepts associés

Chargement

Cours associés

Chargement

Séances de cours associées

Chargement

Résumé

Source officielle

À propos de ce résultat

Publications associées (1)

Publications associées

Chargement

Personnes associées

Chargement

Unités associées

Chargement

Concepts associés (15)

Concepts associés

Chargement

Cours associés (2)

Cours associés

Chargement

Séances de cours associées (4)

Séances de cours associées

Chargement

Cerebellar Ataxia and Coenzyme Q Deficiency through Loss of Unorthodox Kinase Activity

Deniz Aydin, Matteo Dal Peraro, Xiao Guo

The UbiB protein kinase-like (PKL) family is widespread, comprising one-quarter of microbial PKLs and five human homologs, yet its biochemical activities remain obscure. COQ8A (ADCK3) is a mammalian UbiB protein associated with ubiquinone (CoQ) biosynthesis and an ataxia (ARCA2) through unclear means. We show that mice lacking COQ8A develop a slowly progressive cerebellar ataxia linked to Purkinje cell dysfunction and mild exercise intolerance, recapitulating ARCA2. Interspecies biochemical analyses show that COQ8A and yeast Coq8p specifically stabilize a CoQ biosynthesis complex through unorthodox PKL functions. Although COQ8 was predicted to be a protein kinase, we demonstrate that it lacks canonical protein kinase activity in trans. Instead, COQ8 has ATPase activity and interacts with lipid CoQ intermediates, functions that are likely conserved across all domains of life. Collectively, our results lend insight into the molecular activities of the ancient UbiB family and elucidate the biochemical underpinnings of a human disease.

Cell Press2016

Chargement

CS-452: Foundations of software

The course introduces the foundations on which programs and programming languages are built. It introduces syntax, types and semantics as building blocks that together define the properties of a program part or a language. Students will learn how to apply these concepts in their reasoning.

CS-550: Formal verification

We introduce formal verification as an approach for developing highly reliable systems. Formal verification finds proofs that computer systems work under all relevant scenarios. We will learn how to use formal verification tools and explain the theory and the practice behind them.

Assistant de preuve

En informatique (ou en mathématiques assistées par informatique), un assistant de preuve est un logiciel permettant la vérification de preuves mathématiques, soit sur des théorèmes au sens usuel des m

Théorie des types

En mathématiques, logique et informatique, une théorie des types est une classe de systèmes formels, dont certains peuvent servir d'alternatives à la théorie des ensembles comme fondation des mathéma

Correspondance de Curry-Howard

La correspondance de Curry-Howard, appelée également isomorphisme de Curry-de Bruijn-Howard, correspondance preuve/programme ou correspondance formule/type, est une série de résultats à la frontière e