Lean (assistant de preuve)

À propos
Confidentialité
Mentions légales

Graph Chatbot

Séances de cours associées (16)

Connectez-vous pour filtrer par séance de cours

Page 1 sur 2

Atelier Coq: Introduction au théorème interactif

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

Coq: Vue d'ensemble

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

Vérification des programmes avec l'inox

Explore la vérification des programmes en utilisant l'inox, en mettant l'accent sur l'exactitude fonctionnelle, les assistants d'épreuve et l'automatisation des tâches de raisonnement.

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.

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.

Assistant à la preuve de la LISA : formalisation et vérification

Couvre l'organisation de la base de code de l'assistante d'épreuve LISA, le paquet noyau, la formalisation FOL et le paquet d'épreuves.

Abstraction de données : modules et spécifications dans Coq

Discute de l'abstraction des données dans la programmation, en se concentrant sur les modules et les spécifications dans Coq.

Coq: Introduction

Présente Coq, couvrant la définition des propositions, la démonstration des théorèmes, et l'utilisation de 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.

Raisonnement automatisé : vérification formelle avec LISA

Examine la vérification formelle à l'aide de l'assistant d'épreuve LISA et du vérificateur d'équivalence OCBSL.