Commit graph

109 commits

Author SHA1 Message Date
REMY Didier c24814e9bb merge 2017-10-27 10:40:08 +02:00
REMY Didier 12d27e9bfd Slides du cours 2. 2017-10-27 10:38:45 +02:00
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