Update

eb has been partially implemented. The "logic programming" part has been completed; we currently are working on the value-return mechanism.

A paper has been submitted to POPL!

The Programming Language eb

eb is a meta-programming language designed for verifiable programs in computational science and engineering. For more on CSE see "Science, Computational Science, and Computer Science" or the CSE homepage.

The goal is to provide a language that is truly constructive in nature and that contains enough information to correctly generate code in a variety of implemented languages such as C and Fortran. To do so, we have incorporated features similar to traits in Larch. The compiler itself is built around the use of Floyd-Hoare and denotational semantics. To provide a truly constructive approach, we have incorporated backtracking as a means of handling lifted domains. See assembler documents.

Pointers to the Literature

Requests for information about systems usually gets URLs. Here is the list I received from a recent query for information.

Functional Logic Programming
Functional Programming Archive
How to Translate Moded Prolog into Haskell List Comprehensions
F. G. McCabe. Logic and Objects. Prentice-Hall.
Christian Prehofer. Solving Higher-order Equations: From Logic to Programming. PhD Thesis. TU M{\"u}nchen. Number I9508. 1995.
Christian Prehofer. Higher-order Narrowing. In Proc. Ninth Annual IEEE Symposium on Logic in Computer Science. 1994. 507-516
Christian Prehofer. Higher-Order Narrowing with Convergent Systems. AMAST '95. 1995.

Watch this file for more information. If interested in participating in the development of eb, contact

Dr. D. E. Stevenson CC: (Stevenson)