CiteULike is a free online bibliography manager. Register and you can start organising your references online.
Tags

RZ: a Tool for Bringing Constructive and Computable Mathematics Closer to Programming Practice

by: Andrej Bauer, Christopher A. Stone
J Logic Computation, Vol. 19, No. 1. (1 February 2009), pp. 17-43, doi:10.1093/logcom/exn026  Key: citeulike:5454188

Formatted Citation


Show HTML

Likes (beta)

This copy of the article hasn't been liked by anyone yet.

View FullText article


Abstract

Realizability theory is not just a fundamental tool in logic and computability. It also has direct application to the design and implementation of programs, since it can produce code interfaces for the data structure corresponding to a mathematical theory. Our tool, called RZ, serves as a bridge between the worlds of constructive mathematics and programming. By using the realizability interpretation of constructive mathematics, RZ translates specifications in constructive logic into annotated interface code in Objective Caml. The system supports a rich input language allowing descriptions of complex mathematical structures. RZ does not extract code from proofs, but allows any implementation method, from handwritten code to code extracted from proofs by other tools. 10.1093/logcom/exn026


ConcertRG's tags for this article

Citations (CiTO)

No CiTO relationships defined

Xnote Notes for this article (1 public)


X There are no reviews yet

X Find related articles with these CiteULike tags

X Posting History


X Export records

Privacy Statement | Terms & Conditions
CiteULike organises scholarly (or academic) papers or literature and provides bibliographic (which means it makes bibliographies) for universities and higher education establishments. It helps undergraduates and postgraduates. People studying for PhDs or in postdoctoral (postdoc) positions. The service is similar in scope to EndNote or RefWorks or any other reference manager like BibTeX, but it is a social bookmarking service for scientists and humanities researchers.