教程列表¶
Agda 介绍¶
- Ulf Norell and James Chapman.
- Dependently Typed Programming in Agda. This is aimed at functional programmers.
- Ana Bove and Peter Dybjer.
- Dependent Types at Work. A gentle introduction including logic and proofs of programs.
- Ana Bove, Peter Dybjer, and Ulf Norell.
- A Brief Overview of Agda - A Functional Language with Dependent Types (in TPHOLs 2009) with an example of reflection. Code
- Yoshiki Kinoshita.
- Anton Setzer.
- Lecture notes on Interactive Theorem Proving. Swansea University. These lecture notes are based on Agda and contain an introduction of Agda for students with a very basic background in logic and functional programming.
- Daniel Peebles.
- Introduction to Agda. Video of talk from the January 2011 Boston Haskell session at MIT.
- Conor McBride.
- Introduction to Dependently Typed Programming using Agda. (videos of lectures). Associated source files, with exercises.
- Andreas Abel.
- Agda lecture notes. Lecture notes used in teaching functional programming: basic introduction to Agda, Curry-Howard, equality, and verification of optimizations like fusion.
- Jan Malakhovski.
- Thorsten Altenkirch.
- Computer Aided Formal Reasoning - online lecture notes
- Daniel Licata.
- Dependently Typed Programming in Agda (OPLSS 2013).
- Phil Wadler.
- Aaron Stump.
- Diviánszky Péter.
使用 Agda 的课程¶
- Computer Aided Reasoning Material for a 3rd / 4th year course (g53cfr, g54 cfr) at the university of Nottingham 2010 by Thorsten Altenkirch
- Type Theory in Rosario Material for an Agda course in Rosario, Argentina in 2011 by Thorsten Altenkirch
- Software System Design and Implementation , undergrad(?) course at the University of New South Wales by Manuel Chakravarty.
- Seminar on Dependently Typed Programming , course at Utrecht University by Andres Löh.
- Tüübiteooria / Type Theory , graduate course at the University of Tartu by Varmo Vene and James Chapman.
- Advanced Topics in Programming Languages: Dependent Type Systems , course at the University of Pennsylvania by Stephanie Weirich.
- Categorical Logic , course at the University of Cambridge by Samuel Staton. - More info and feedback
- Dependently typed functional languages , master level course at EAFIT University by Andrés Sicard-Ramírez.
- Introduction to Dependently Typed Programming using Agda , research level course at the University of Edinburgh by Conor McBride.
- Agda , introductory course for master students at ELTE Eötvös Collegium in Budapest by Péter Diviánszky and Ambrus Kaposi.
- Types for Programs and Proofs , course at Chalmers University of Technology.
- Advanced Functional Programming (in German), course at Ludwig-Maximilians-University Munich.
- Dependently typed metaprogramming (in Agda) , Summer (2013) course at the University of Cambridge by Conor McBride.
- Computer-Checked Programs and Proofs (COMP 360-1), Dan Licata, Wesleyan, Fall 2013.
- Advanced Functional Programming (CS410), Conor McBride, Strathclyde, Fall 2013.
- Interactive Theorem proving (CS__336), Anton Setzer, Swansea University, Lent 2008.
- Inductive and inductive-recursive definitions in Intuitionistic Type Theory , lectures by Peter Dybjer at the Oregon Programming Languages Summer School 2015.