*for AIM XVI*

Let people play and explore some programming in Agda without theoretical background.

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.
- The proposed tutorial is a demonstration for this.

- Much background theoretical remarks interrupts the playing 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.
- We give pointers on a separate page.

There are pointers on that page into the tutorial.

- We give pointers on a separate page.

**Subgoals**- Give the semantics of Agda programs by examples.
- Teach Agda programming skills.
- when to use which language construct

- Give a methodology to write correct Agda programs.
- what does program correctness mean
- how to be more sure that the program is correct

**Requirements**- Only secondary school mathematics is required.
- no Haskell, type theory, category theory, ...
- followable without a tutor

**Audience**- - for newcomers

This is the 4th semester we teach Agda at ELTE Budapest.

- 13 week × 90 min
- 3-8 students
- Lecturers: Péter Diviánszky and Ambrus Kaposi*
- The course material is revised each semester.

*We also learn as we teach which may be inspired this practical tutorial.

Tutorial: *Idiomatic solutions for practical exercises taken into pieces, sorted and explained.*

- Collect interesting exercises for students
- practical problems like
**roman numerals, leap years, ...**

- practical problems like
- Write idiomatic Agda solutions for the problems.
**specification**(mainly with data types)- implementation (functions)

- Take the solutions into incremental pieces.
- essential problems like sorting should appear here!

- Sort the pieces by the language constructs/techniques used.
**data types first, functions later**- ...

- Fill in semantic gaps with ad-hoc exercises.
- revisit non-idiomatic code when the idiomatic solution is possible
- try to
**avoid this step**

- Hide all Agda code!

Unhide code for the first appearance of any language construct/technique used and add**very practical explanations**.

The emphasised parts are the features of this tutorial, especially what kind of problems we take in the 1st step.

We can improve at every step 1-6 which explains that the tutorial is rewritten every time.

- remain freely available and ready to fork
*Problem:*we have to give univ. students different exercises...

- give citation of sources if applicable
- try to merge with similar tutorials if any

- Only ~1/6 is ready.
- The methodology is not strictly followed yet.
- There are too much ad-hoc exercises.

- Currently Peter is working on it.

The darcs repository is located at http://hub.darcs.net/divip/AgdaTutorial

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

We visit the current tutorial.

Thank you for any feedback.