Logical frameworks - PhD course

Contents

Schedule

1. Friday 19/9, 10.30-12.15 in room 3513, Department of Math., MIC, Polacksbacken
2. Friday 26/9, same time and place
3. Friday 3/10, same time and place

   Project work.

4. Friday 28/11, 10.30-12.15, (conference) room 3412, Dept. Math.
5. Friday 5/12, 10.30-12.15, (conference) room 3311, Dept. Math.

   Christmas break.

   There will be two additional lectures on semantics of type theories. We will partly follow Martin Hofmann's lecture notes Syntax and semantics of dependent types, In: Semantics of Logics of Computation, P. Dybjer and A. Pitts, eds., Cambridge University Press. 1997.

6. Friday 6/2, 10.30-12.15 in room 3513.
7. Wednesday 17/2, 13.15-15.00 in room 3513. (Final lecture. No further scheduled events.)

Examples, Exercises and Problems in Agda

1. Some exercises from an elementary textbook (Hansen's Grundläggande logik) with solutions.
2. PROBLEM 1: to be E-MAILED in solved Agda-format to me by Friday SEPTEMBER 26.
3. Example illustrating general recursive data types as opposed to inductive data types. How to arrive at a paradox using recursive data types. Recursive data types are detected by the termination checker and a warning is issued. However, it also raises a false alarm for some legitimate inductive types.
4. PROBLEMS 2 and 3: to be E-MAILED in solved Agda-format to me by Friday OCTOBER 3.
5. The natural numbers as a setoid and some basic lemmas: NaturalsSE.agda Note that x+ S0 = S x is true as definitional equality, while S0 + x = S x is not. Such differences disappears for the setoid equality.
6. Until Friday Oct. 3, think about some project from the list of suggestions, or invent a project of reasonable size yourself.
7. Binary.agda implements the structure (N,=,*,+) of natural numbers as binary numbers, and contains a proof that it is isomorphic to the unary representation.
8. TheoryAsPackage_ex1.agda illustrates how a bunch of related definition and theorems, e.g. a theory, may be collected into what is known as a "package". It is strongly recommended that you use this feature in larger proofs.
9. Learn how to make abbreviations, using "let", definitions in sigma types and packages. Look at the library "New", which comes with the latest distribution, for some further examples and inspiration. See also the examples in the Agda documentation.
10. Use abstractions to make your results independent of representation. This can be achieved using sigma types describing the properties of a certain structure. Some times all such structures are isomorphic. This may be expressed in categorical language. For the example of the free monoid over a set, see Monoid_ex2.agda .
11. Extensionality.agda contains a suggestion how to deal with extensionality of compound expression, e.g. a setoid-equality inside a formula. You can almost mechanically derive extensionality of a complex formula in a certain variable by looking at its structure and applying AllExt, ConstExt, OrExt etc.
12. E_categories_two_sizes.agda contains a common definition of categories, small and locally small. Use the UPDATED version of SE.agda.

Projects

Agda

Lecturer

• Erik Palmgren.

This page is : www2.math.uu.se/~palmgren/frameworks