Home
Education Page
Course schedule
Assignments
Papers
VerificationChallenge
Agda
Coq
Center
Home
Courses
People
Projects
Page
Edit Page
Rename Page
Attach File
Printable
Wiki Source
More ...
Web
Recent Changes
Notify Service
News
Page Index
Search
More ...
Wiki
About TWiki
Text Formatting
Registration
Change Password
Reset Password
Users
Groups
Log In
or
Register
Agda
DTP
The programming language we will use throughout the second part of this course. Agda2 is a dependently typed programming language with a specific focus on _programming_ rather than _theorem proving_. Of course, like other languages based on dependent types, it allows to specify and prove properties. But currently, there are more convenience features for writing executable programs than for verifying complex properties. ---++ Homepage The [[http://appserv.cs.chalmers.se/users/ulfn/wiki/agda.php][homepage of Agda]] is a Wiki at Chalmers. ---++ Installation Ideally, you can install Agda via Cabal. We will work with version 2.3.2 of Agda. For further information, there is a [[http://appserv.cs.chalmers.se/users/ulfn/wiki/agda.php?n=Main.Download][Wiki page]] that explains how to install Agda. It also lists the required software. ---++ Tutorials Look [[http://wiki.portal.chalmers.se/agda/agda.php?n=Main.Othertutorials][here]]. We will mainly use the tutorial by Ulf Norell. -- Main.WouterSwierstra - 23 Apr 2013