Programming assurance cases in Agda

Abstract

Agda is a modern functional programming language equipped with an interactive proof assistant as its developing environment. Its features include dependent types, type universe, inductive and coinductive families of types, pattern matching, records, and nested parameterized modules. Based on the "propositions as types, proofs as programs" correspondence in Martin-Löf's Type Theory, Agda lets users to construct, verify, and execute a smooth mixture of programs and proofs.