# References

* [Programming Language Foundations in Agda](https://plfa.github.io/) -- by Philip Wadler, Wen Kokke and Jeremy Siek
* [Programming and Proving in Agda](https://github.com/jespercockx/agda-lecture-notes/raw/master/agda.pdf) -- by Jesper Cockx
* [Introduction to Univalent Foundations of Mathematics with Agda](https://www.cs.bham.ac.uk/~mhe/HoTT-UF-in-Agda-Lecture-Notes/index.html) -- by Martín Escardó
* [Dependent Types at Work](http://www.cse.chalmers.se/~peterd/papers/DependentTypesAtWork.pdf) -- by Ana Bove and Peter Dybjer
* [Learn you an Agda](https://williamdemeo.github.io/2014/02/27/learn-you-an-agda/) -- by Liam O'Connor-Davis with additions by William DeMeo
* [A practical Agda tutorial](https://people.inf.elte.hu/divip/AgdaTutorial/Index.html) -- by Péter Diviánszky and Ambrus Kaposi
* [Correct-by-construction programming in Agda](https://jespercockx.github.io/ohrid19-agda/) -- by Jesper Cockx
* [More on the double-negation translation](https://www.speicherleck.de/iblech/stuff/slides-fischbachau2022.pdf)
* [Interactive Theorem Proving](https://p8.cs.fau.de/itp/) -- by Thorsten Wißmann
* [1Lab](https://1lab.dev/) -- by Amélia Liao and collaborators
* [TypeTopology](https://martinescardo.github.io/TypeTopology/) -- by Martín Escardó and collaborators


<!--
```
{-# OPTIONS --cubical-compatible #-}
module Padova2025.Welcome.References where
```
-->