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.