for AIM XVI

Goal

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

Ideology

Assumptions

Goal details

Subgoals
Requirements
Audience
- for newcomers

Resources

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


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

Planned methodology

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

  1. Collect interesting exercises for students
  2. Write idiomatic Agda solutions for the problems.
    1. specification (mainly with data types)
    2. implementation (functions)
  3. Take the solutions into incremental pieces.
  4. Sort the pieces by the language constructs/techniques used.
  5. Fill in semantic gaps with ad-hoc exercises.
  6. 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.

Social contract

State of art

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

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

Demo

We visit the current tutorial.

Thank you for listening!

Thank you for any feedback.