參考資料#

• Programming Language Foundations in Agda – 作者：Philip Wadler、Wen Kokke 與 Jeremy Siek
• Programming and Proving in Agda – 作者：Jesper Cockx
• Introduction to Univalent Foundations of Mathematics with Agda – 作者：Martín Escardó
• Dependent Types at Work – 作者：Ana Bove 與 Peter Dybjer
• Learn you an Agda – 作者：Liam O’Connor-Davis，William DeMeo 補充
• A practical Agda tutorial – 作者：Péter Diviánszky 與 Ambrus Kaposi
• Correct-by-construction programming in Agda – 作者：Jesper Cockx
• More on the double-negation translation
• Interactive Theorem Proving – 作者：Thorsten Wißmann
• 1Lab – 作者：Amélia Liao 與其他協作者
• TypeTopology – 作者：Martín Escardó 與其他協作者