Commit 99034327 authored by Pierre Letouzey's avatar Pierre Letouzey
Browse files

expose, suite

parent 7f9036ad
......@@ -2,6 +2,14 @@
% Pierre Letouzey
% 3 septembre 2019
## L'informatique, ça peut être assez fumeux...
\includegraphics[width=\linewidth]{tabacchi.jpg}
## En cas de doute, suivre le chemin canonique ...
\includegraphics[width=\linewidth]{piombino_via_canonica.jpg}
## Pointeurs
- Le cours de "preuves assistées par Ordinateur" (Master1 ici) : <https://www.irif.fr/users/letouzey/edu/preuves>
......@@ -40,29 +48,6 @@ Pas de doute envers ces résultats très standards. Mais:
<https://www.isa-afp.org/entries/Completeness-paper.pdf>
## Lignes de code Coq
```
201 AsciiOrder.v + StringOrder.v
526 StringUtils.v + Utils.v
424 NameProofs.v
562 Countable.v
187 Defs.v
542 Nam.v
934 Mix.v
258 Subst.v
1175 Equiv.v + Equiv2.v
1842 Meta.v
1334 Theories.v
466 PreModels.v
956 Models.v
167 Peano.v
116 FormulaReader.v
1194 AltSubst.v
10884 total
```
## Un aperçu du poly d'origine
Cf <https://www.irif.fr/~letouzey/preuves/cours.pdf>
......@@ -102,6 +87,29 @@ Shallow Embedding / Deep Embedding ?
- locally nameless
- ...
## Lignes de code Coq
```
201 AsciiOrder.v + StringOrder.v
526 StringUtils.v + Utils.v
424 NameProofs.v
562 Countable.v
187 Defs.v
542 Nam.v
934 Mix.v
258 Subst.v
1175 Equiv.v + Equiv2.v
1842 Meta.v
1334 Theories.v
466 PreModels.v
956 Models.v
167 Peano.v
116 FormulaReader.v
1194 AltSubst.v
10884 total
```
## Visite guidée des fichiers Coq
## Conclusions & Perspectives
......
No preview for this file type
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment