Dept. of Computer Science

University of Wales Swansea

Singleton Park

Swansea

SA2 8PP,UK

Tel. (01792) 513368

Fax (01792) 295651

- Tuesday, 12:00, Faraday B
- Thursday, 12:00, Faraday C

- In order to read and print out pdf-files, you need a PDF reader. For instance Acrobat Reader is available free here:
- For my students: Please
**don't print these files on departmental printers**. Instead ask in the student secretary for a copy. To print out on ordinary printers costs, because of the cost of the toner,**5 to 10 times more**than fotocopying, as done by the lecturer. **Full Version.**

Contains some material which is only available to students taking this course. (You won't miss much if you don't have access to this version).

Please press the login button. If your password is not correct, you will be redirected to a non-existing page.

(You might need to enable java script on your browser - for Internet Explorer see this page for instructions; especially you need to enable "Allow websites to prompt for information using scrpted windows")

- Slides by section
- Errata
- Section 0: Introduction.
- Section 1: From simple to dependent types.
- Section 2: Reduction systems and term rewriting.
- Section 3: The lambda-calculus and implication (includes a basic introduction into Agda).
- Section 4: The lambda-calculus with products and conjunction
- Section 5: The logical framework.
- Section 6: Data types.
- Old Versions of Sections 3 - 6.

Because of prosper slides no longer being supported, the above Sections 3 - 6 were converted into latex style beamer in order to carry out some minor corrections.

In case of conversion errors, please refer to the original slides using latex style prosper:- Sect. 3 Old
- Sect. 4 Old
- Sect. 5 Old
- Sect. 6 Old

- Agda
- Introductions to Agda
- My slides for CSCM10 on Research in Theoretical Computer Science - Specification and Verification contain in Subsection "Dependent Type Theory" a basic motivation on why to use Agda.
- Video introducing Agda (very suitable for beginners; no sound, everything is explained by typing)
- My Youtube channel with Agda Introductions
- Another video introduction of Agda
- Video introduction to Agda for Haskell programmers
- Agda from nothing
- Dependently typed programming Agda.: An Introduction (by Conor McBride)

- Learn You an Agda and achieve enlightenment!
- Documentation about Agda (from the Agda Wiki; contains links to tutorials and courses teaching Agda and more)
- Book by Aaron Stump: Verified functional programming in Agda (Google Books Entry)
- Agda Wiki (a wikipedia, only for Agda; contains most documentation, installation instructions, information about Agda Implementors Meetings, tutorials, and more)
- Agda (Wikipedia Entry)
- Official Documentation of Agda
- Agda Change log contains the most recent additions of Agda, many of which are not part of the documentation yet.
- A shorter version of the introduction to Agda in the lectures above can be found in the Critical Systems slides from 2002/03

- Introductions to Agda
- Material developed by Anton Setzer
- ooAgda library (joint with Andreas Abel and Stephan Adelsberger)
- Examples used in the lecture
- Installation of Agda2
- List of leim symbols under Agda
- Use of the abbreviation mode, which makes typing in special symbols much easier
- Agda reference card (refers still to Agda1)
- Getting started with Agda (refers still to Agda1).

- Alfa main page (doesn't seem to support the new syntax of Agda or Agda2)

- Per Martin Löf: Intuitionistic Type Theory
- Book: Programming in Martin-Löf's Type Theory
- B. Nordström, K. Petersson, J. Smith: Martin-Löf's Type Theory. In: Handbook of Logic in Computer Science. Oxford University Press, 2000.

- Module given in previous years
- Course page Interactive Theorem Proving from 2006/07
- Course page Interactive Theorem Proving from 2005/06
- Course page Interactive Theorem Proving from 2004/05
- Course page Interactive Theorem Proving from 2003/04
- Course page Critical Systems CS_411 from 2002/03 (Stream B relevant for this module)
- Course page Critical Systems CS_411 from 2001/02 (Stream B relevant for this module)

Last modified: Wed Jan 14 14:18:11 GMT 2009