Programming Assurance Cases in Agda

摘要

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-Lof s Type Theory, Agda lets users to construct, verify, and execute a smooth mixture of programs and proofs. Using Agda is similar to using an editor in a modern IDE. Users have more direct control over how programs / proofs are written than in automation-oriented systems using command-scripts for proof construction. Agda thus encourages users to express their ideas with more sophisticated dependently typed programming and less logical proofs. Programming techniques for readability and maintainability now translate to techniques for writing verified documents for human communication. Agda has been developed at Chalmers University of Technology by Ulf Norell and others. A growing international community of developers and users applies it in research, education, and industry. At AIST in Japan, we aim to introduce its merits to construction, verification, maintenance, and run-time evaluation of "assurance cases", which are documented bodies of systems assurance arguments used as the hub for assurance- and risk-communication among stakeholders. The talk gives an overview of Agda and presents our current effort on programming assurance cases in Agda.