Here are three files that have been shown at the lecture and you.You can also make the exercises with Coq.For some more handwritten answers to exercises, see canvas.Higher order logic, Calculus of Constructions Here are some answers to the exercises.Polymorphic Types: ML style and full polymorphism The first three pages of this document describe the principal type algorithm in detail.23/2, No Lecture because of Carnaval holiday.Problem") at home and send it to the teacher by mail by Complete this (you can skip the "Challenge Complete this at home and send it to the teacherĮxercises. Proposition Logic: Here is the file with the.Here are some answers to the exercises and some hand-written worked out Fitch style derivations (for exercises 3 and 4).Ĭoq: proposition logic and predicate logic.īe sure to have Coq installed on your laptop/computer.Here are some answers to the exercises, with a hand-written note on how to do exercise 5c."Formulas-as-Types" for propositional logic. See the syllabus on Canvas for the answers. To Lambda Calculus - selected pages by Barendregt and Barendsen. Verification, Logic, Type Theory, Formulas-as-types, Coq. Overview and Introduction: Proof Assistants, This schedule may be subject to changes! Especially the slides and exercises may be slightly adapted as we go along the course. The course will be recorded and recordings will be provided on Canvas (in the syllabus) on a weekly basis. With all the Coq files about inductive types. Your assignment is a formalization in Coq. Throughout the course we will be showing a number of Coq files andįor some you will need to fill in the proofs yourself as anĮxercise.You have to download and install Coq yourself.We will be using the Proof Assistant Coq in this course. The starting page for Coq documentation.A short tutorial for Coq by Mike Nahas.A short introduction to Coq by the developers.With a list of useful Coq goodies by Jules Jacobs. With a list of simple useful Coq tactics. A quick introduction to Coq, notably read Section 3. On the Coq Proof Assistant: you may find one of the following useful:.The slides of the course, please find the pdfs below.(This is a selection of pages from the full Introduction to Lambda Calculus.) On lambda calculus: Introduction to Lambda Calculus - selected pages by Barendregt and Barendsen.With a "hands on experience": using the proof assistant The course basically covers the material in the book Herman Geuvers) has appeared in November 2014 with Cambridge Theory and Formal Proof - An Introduction (Rob Nederpelt and The material of lectures 2, 3, 5, 6, 13 is To Type Theory by Herman Geuvers, notes of a summer school course Furthermore, read the selected pages of Introduction to Lambda Calculus ofīarendregt and Barendsen, Chapter 1, Chapter 4 pp. I will do a short recapitulation in hour 2 of the Lecture 1. For those not familiar with untyped lambda calculus:.We assume that you are familiar with a bit of logic, especially natural deduction and preferably (untyped) lambda calculus. Room number MF6.079A (only on Thursdays) For contact, use the e-mail address herman at cs dot ru dot nl Location and time Proving with Computer Assistance (Spring 2022) 2IMF15 Proving with Computer Assistance 2IMF15 Teacher
0 Comments
Leave a Reply. |
AuthorWrite something about yourself. No need to be fancy, just an overview. ArchivesCategories |