Mathematics and Computation

A blog about mathematics for computers

Specifications via Realizability (CLASE 2005)

With Chris Stone.

Abstract:
We present a system, called RZ, for automatic generation of program specifications from mathematical theories. We translate mathematical theories to specifications by computing their realizability interpretations in the ML language augmented with assertions (as comments). While the system is best suited for descriptions of those data structures that can be easily described in mathematical language (e.g., finitely presented groups, real arithmetic, graphs, etc.), it also elucidates the relationship between data structures and constructive mathematics.

Presented at:
Constructive Logic for Automated Software Engineering (CLASE), Satellite event of ETAPS 2005, Edinburgh, 9th April 2005

Download paper:
rz.pdf,
rz.ps.gz

Download slides:
rz-slides.pdf

How to comment on this blog: At present comments are disabled because the relevant script died. If you comment on this post on Mastodon and mention andrejbauer@mathstodon.xyz, I will gladly respond. You are also welcome to contact me directly.