To insert individual citation into a bibliography in a word-processor,
select your preferred citation style below and drag-and-drop it into the document.
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.
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
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.