Specifications via Realizability | Zendy

Andrej Bauer | Zendy; C. Addison Stone | Zendy

AI Assistant Blog Pricing

Home ZAIA Blog

Open Access

Specifications via Realizability

Author(s) -

Andrej Bauer,

C. Addison Stone

Publication year - 2006

Publication title -

electronic notes in theoretical computer science

Language(s) - English

Resource type - Journals

SCImago Journal Rank - 0.242

H-Index - 60

ISSN - 1571-0661

DOI - 10.1016/j.entcs.2005.08.007

Subject(s) - realizability , constructive , computer science , programming language , algebra over a field , arithmetic , theoretical computer science , calculus (dental) , mathematics , pure mathematics , medicine , dentistry , process (computing)

We present a system, called RZ, for automatic generation of program specifications from mathemat- ical 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 mathemat- ical language (e.g., finitely presented groups, real arithmetic, graphs, etc.), it also elucidates the relationship between data structures and constructive mathematics

The content you want is available to Zendy users.

Already have an account? Click here to sign in.

Having issues? You can contact us here

Accelerating Research