Verified programming in Guru

Aaron Stump; Morgan Deters; Adam Petcher; Todd Schiller; Timothy Simpson

doi:10.1145/1481848.1481856

Back

Conference proceeding

Verified programming in Guru

Aaron Stump, Morgan Deters, Adam Petcher, Todd Schiller and Timothy Simpson

Proceedings of the 3rd workshop on programming languages meets program verification, pp.49-58

PLPV '09

01/20/2009

DOI: 10.1145/1481848.1481856

View Online

Abstract

Operational Type Theory (OpTT) is a type theory allowing possibly diverging programs while retaining decidability of type checking and a consistent logic. This is done by distinguishing proofs and (program) terms, as well as formulas and types. The theory features propositional equality on type-free terms, which facilitates reasoning about dependently typed programs. OpTT has been implemented in the Guru verified programming language, which includes a type- and proof-checker, and a compiler to efficient C code. In addition to the core OpTT, Guru implements a number of extensions, including ones for verification of programs using mutable state and input/output. This paper gives an introduction to verified programming in Guru.

dependently typed programming

language-based verification

operational type theory

Details

Title: Subtitle: Verified programming in Guru
Creators: Aaron Stump - University of Iowa
Morgan Deters - Universitat Politècnica de Catalunya
Adam Petcher - Washington University in St. Louis
Todd Schiller - Washington University in St. Louis
Timothy Simpson - Washington University in St. Louis
Resource Type: Conference proceeding
Publication Details: Proceedings of the 3rd workshop on programming languages meets program verification, pp.49-58
Series: PLPV '09
DOI: 10.1145/1481848.1481856
Publisher: ACM
Language: English
Date published: 01/20/2009
Academic Unit: Computer Science
Record Identifier: 9984259491802771

Metrics

6 Record Views