You are here:
(23 Apr 2013, WouterSwierstra)
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
ore topic actions
Topic revision: r10 - 23 Apr 2013, WouterSwierstra
Copyright © by the contributing authors. All material on this collaboration platform is the property of the contributing authors.
Ideas, requests, problems regarding UUCS?