Proving Program Properties Automatically With Agda Light
Stc
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.- AgdaLight homepage: http://www.cs.chalmers.se/~ulfn/agdaLight/
- Presentation slides: agdalight.pdf