Towards a framework for formal assurance cases in Agda

Makoto Takeyama

Kanagawa University

Wednesday, 15 October 2014, 14:30 (note the unusual weekday and time)
Cybernetica Bldg (Akadeemia tee 21), room B401

Slides from the talk [pdf]

Abstract: A formulation of assurance cases in Agda language is presented, which enables Correctness by Construction approach to assurance cases. The routine consistency checking is done by Agda type checker, so that the human reviewer can concentrate on their judgment on contents. Moreover, the module system and other programming language features of Agda provides the structuring and abstraction mechanisms for assurance cases necessary for higher readability and maintainability in the large.

Tarmo Uustalu
Last update 5 November 2014