You are here:
(02 Sep 2010,
Date: 2007-11-15 Time: 11:45 Room: BBL room 471 ----+++ Speaker: Kasper Brink ----+++ Title: Proving Program Properties Automatically with !AgdaLight ----+++ Abstract Stating properties of programs, and proving them, can increase our confidence in the correctness of those programs. Dependently typed programming languages offer a natural way to express both properties and their proofs. However, proofs often contain many simple reasoning steps that are tedious to write by hand. We would like the system to perform such low-level steps automatically, allowing the programmer to focus on the high-level structure of the proof. !AgdaLight is a prototype language with a dependent type system and a Haskell-like syntax. It has a plugin mechanism that enables sending first-order goals to an external theorem prover. In this talk we will introduce !AgdaLight and show how to prove properties with it through several examples. <!-- * Set PREV_SKIN = customtitle * Set CUSTOMTOPICTITLE = Proving Program Properties Automatically with !AgdaLight * Set CUSTOMHEADTITLE = Stc / Proving Program Properties Automatically with !AgdaLight --> * !AgdaLight homepage: http://www.cs.chalmers.se/~ulfn/agdaLight/ * Presentation slides: [[%ATTACHURL%/agdalight.pdf][agdalight.pdf]]
ore topic actions
Topic revision: r3 - 02 Sep 2010,
Copyright © by the contributing authors. All material on this collaboration platform is the property of the contributing authors.
Ideas, requests, problems regarding UUCS?