François Pottier
|
054e451133
|
Fix the statement of rule SR1.
|
2017-10-20 21:00:49 +02:00 |
|
François Pottier
|
639d7951fc
|
Link to Coq mini-demo.
|
2017-10-20 12:38:59 +02:00 |
|
François Pottier
|
9db653f644
|
Expose today's slides.
|
2017-10-20 11:28:57 +02:00 |
|
François Pottier
|
aeedf926d4
|
Add today's slides.
|
2017-10-20 11:28:18 +02:00 |
|
François Pottier
|
c0c83a490d
|
Add a demo of equational reasoning in Coq.
|
2017-10-20 10:36:47 +02:00 |
|
François Pottier
|
8d78692d88
|
Nested lists.
|
2017-10-13 09:28:58 +02:00 |
|
François Pottier
|
de8d6fedd9
|
Add today's slides.
|
2017-10-13 09:26:06 +02:00 |
|
François Pottier
|
521f29c442
|
README.
|
2017-10-12 15:47:05 +02:00 |
|
François Pottier
|
8c50463ec4
|
New OCaml exercise.
|
2017-10-12 15:40:11 +02:00 |
|
François Pottier
|
b88b92d33c
|
Add new OCaml files.
|
2017-10-11 19:47:20 +02:00 |
|
François Pottier
|
555822838f
|
Add the Coq formalization of the CPS transformation.
|
2017-10-11 15:28:20 +02:00 |
|
François Pottier
|
79af3f8d1c
|
Removed MetaBigStep.v -- a typo in a file name.
|
2017-10-11 15:27:50 +02:00 |
|
François Pottier
|
63e854b686
|
Fix another typo in last week's slides.
|
2017-10-10 17:35:30 +02:00 |
|
François Pottier
|
61209d310e
|
Fix a typo in today's slides.
|
2017-10-06 16:20:46 +02:00 |
|
François Pottier
|
318919da17
|
Link to today's slides.
|
2017-10-06 12:33:23 +02:00 |
|
François Pottier
|
c61a164474
|
Today's slides.
|
2017-10-06 11:22:54 +02:00 |
|
François Pottier
|
083c0c1843
|
Expose new Coq files.
|
2017-10-05 17:57:33 +02:00 |
|
François Pottier
|
42ddbb4f1e
|
Updated last slide.
|
2017-09-29 23:51:03 +02:00 |
|
François Pottier
|
a6d9506bd0
|
Links from README.md to the slides and OCaml/Coq files.
|
2017-09-29 17:32:32 +02:00 |
|
François Pottier
|
fb3e42ac0d
|
New slides. New file ocaml/Lambda.ml.
|
2017-09-29 11:21:20 +02:00 |
|
François Pottier
|
548479586f
|
Remove marks in Coq files.
|
2017-09-28 15:15:51 +02:00 |
|
François Pottier
|
b69e9ec88f
|
Add coq/README.md.
|
2017-09-28 10:36:55 +02:00 |
|
François Pottier
|
213264633f
|
Expose more Coq files.
|
2017-09-28 10:36:07 +02:00 |
|
François Pottier
|
3e3eabe58a
|
Added Even.v.
|
2017-09-26 16:50:45 +02:00 |
|
François Pottier
|
9903510037
|
A few improvements in last week's slides.
|
2017-09-26 11:42:59 +02:00 |
|
François Pottier
|
f31a263ff7
|
Updated slides, Coq demo, and OCaml exercise.
|
2017-09-22 11:32:50 +02:00 |
|
François Pottier
|
cb1a56bbda
|
Indicate how to load ProofGeneral in .emacs.
|
2017-09-21 22:09:04 +02:00 |
|
François Pottier
|
09761828fc
|
Clarified installation instructions. Added instructions for ProofGeneral.
|
2017-09-21 22:04:18 +02:00 |
|
François Pottier
|
03e6914d0f
|
The Coq demo does not need MyTactics.
|
2017-09-21 21:42:18 +02:00 |
|
François Pottier
|
86c981fb99
|
Publish slides 01a and 01b. Links from README.
|
2017-09-21 21:29:24 +02:00 |
|
François Pottier
|
845312be45
|
Coq demo.
|
2017-09-21 15:40:42 +02:00 |
|
François Pottier
|
906c153fb9
|
Link to my introductory slides.
|
2017-09-21 11:06:57 +02:00 |
|
François Pottier
|
7b95f194ea
|
Introductory slides.
|
2017-09-21 11:05:14 +02:00 |
|
François Pottier
|
165e637bc5
|
Instructions for installing AutoSubst.
|
2017-09-20 15:51:16 +02:00 |
|
François Pottier
|
ace98b8d7a
|
English. (Plus spurious whitespace.)
|
2017-09-20 15:48:34 +02:00 |
|
REMY Didier
|
20967ac671
|
./2016/ -> ./
|
2017-09-20 13:50:54 +02:00 |
|
REMY Didier
|
672cfcd07d
|
slides and notes
|
2017-09-15 08:55:27 +02:00 |
|
REMY Didier
|
997801873b
|
slides and notes
|
2017-09-15 08:52:43 +02:00 |
|
REMY Didier
|
1bd9634a2a
|
slides and notes
|
2017-09-15 08:49:14 +02:00 |
|
REMY Didier
|
d235435edb
|
duration
|
2017-09-14 18:11:11 +02:00 |
|
REMY Didier
|
873f1cfde1
|
backpointer
|
2017-09-14 16:35:49 +02:00 |
|
REMY Didier
|
98cf311208
|
urls
|
2017-09-14 15:22:47 +02:00 |
|
REMY Didier
|
88a9804cab
|
urls
|
2017-09-14 15:20:36 +02:00 |
|
REMY Didier
|
85ceb49c7d
|
url
|
2017-09-14 15:18:16 +02:00 |
|
REMY Didier
|
6e18628cae
|
Previous Exams
|
2017-09-14 15:12:03 +02:00 |
|
REMY Didier
|
599d85f58d
|
+biblio, course content
|
2017-09-14 11:22:15 +02:00 |
|
REMY Didier
|
4cceeb632a
|
Correction de dates
|
2017-09-11 11:55:20 +02:00 |
|
François Pottier
|
1a926bb89d
|
Typo.
|
2017-09-11 11:07:05 +02:00 |
|
François Pottier
|
1df18e3832
|
.gitignore.
|
2017-09-11 10:50:45 +02:00 |
|
François Pottier
|
51b07afefc
|
Bibliography.
|
2017-09-11 10:50:20 +02:00 |
|