Coq (logiciel)

Science formelle
Informatique théorique
Théorie des langages de pro...
Théorie des types

À propos
Confidentialité
Mentions légales

Graph Chatbot

Séances de cours associées (29)

Connectez-vous pour filtrer par séance de cours

Page 1 sur 3

Coq: Vue d'ensemble

Présente Coq et se concentre sur la démonstration du théorème et du _comm étape par étape.

Propositions inductives : comprendre l’évaluation dans Coq

Couvre les propositions inductives en Coq, en se concentrant sur les règles dévaluation pour les expressions arithmétiques et leurs applications dans la définition des fonctions partielles et non déterministes.

Atelier Coq: Introduction au théorème interactif

Introduit Coq, un assistant de théorème interactif basé sur l'isomorphisme de Curry-Howard.

Techniques de programmation logique: Recherche et unification automatisées de preuves

Couvre les concepts de programmation logique, en se concentrant sur la recherche de preuve automatisée et les techniques d'unification dans Coq.

Introduction à Coq: Expressions arithmétiques et évaluateurs

Couvre les bases de Coq, en se concentrant sur les expressions arithmétiques, l'évaluation et les techniques de preuve.

Introduction aux scripts de preuve: bases de Ltac

Présente les bases du script de preuve en Coq, en se concentrant sur le langage Ltac et ses tactiques pour gérer efficacement les preuves.

Coq: Introduction

Présente Coq, couvrant la définition des propositions, la démonstration des théorèmes, et l'utilisation de tactiques.

Programmes de vérification avec l'inox: Comment fonctionne l'inox

Explore le fonctionnement intérieur du cadre Inox, en mettant l'accent sur les transformations de vérification et de contrôle de type dépendant.

Atelier Coq: Types de données inductives et preuves

Couvre la définition d'un type de données inductives dans Coq et la façon de construire des preuves de manière interactive en utilisant des tactiques.

Polymorphisme dans Coq: Structures de données et fonctions

Couvre le polymorphisme dans Coq, en se concentrant sur les structures de données et les fonctions telles que les listes, la longueur et l'ajout.