Goal

Let people explore programming in Agda without theoretical background.

Ideology

Assumptions

• Most IT people are not interested in theory in the first place.
• One can go a long way without any theoretical knowledge in Agda.
  
• Theoretical remarks interrupt the programming experience.
  • Students react quite differently to theoretical remarks.
    (confused ↔ want to know a lot more)
• People who already played with Agda are more open to theoretical background.

Goal details

Subgoals

• give the syntax and semantics of Agda by examples
• teach Agda programming skills

Requirements

• Only secondary school mathematics is required.
• Haskell, type theory and category theory knowledge is not required.

Audience

• for newcomers

- followable without a tutor

How to teach programming skills

• The programmers should know equivalent solutions to be able to make design decisions.
  We teach program transformations steps.
• The programmers should know which solution is better to be able to make design decisions.
  We add remarks to each program transformation steps.
• We teach how to do incremental program construction (planned).

Additional features

• teach data types first, functions later

Darcs repository

The darcs repository is located at

http://hub.darcs.net/divip/AgdaTutorial

You are welcome to send patches (please send small patches first)!

Social contract

• remain freely available and ready to fork
• give citation of sources if applicable
• try to merge with similar tutorials if any

Users

This is the 5th semester we teach Agda at ELTE Budapest with the help of this tutorial.

• 13 week × 90 min
• Lecturers: Péter Diviánszky and Ambrus Kaposi
  • we also learn a lot by teaching Agda

Other material

import About.AIM_XVI     -- The original slides for AIM XVI.