User loginNavigation |
A reflective functional language for hardware design and theorem provingJ. Grundy, T. Melham, and J. O'Leary, A reflective functional language for hardware design and theorem proving, Journal of Functional Programming, 16(2):157-196, March 2006. This paper introduces reFLect, a functional programming language with reflection features intended for applications in hardware design and verification. The reFLect language is strongly typed and similar to ML, but has quotation and antiquotation constructs. These may be used to construct and decompose expressions in the reFLect language itself. reFLect is apparently a follow-on to the earlier FL language (which I asked about in an earlier thread), the language used in Intel's Forte hardware verification environment. Within Forte, reFLect can be used to perform a seamless mix of theorem proving and model-checking (invocation of a model-checker is just a reFLect function call, with the source text of any call to the model-checker that returns true becoming a theorem of the logic). Tom Melham's reFLect page has a little more information, and also points out that a Linux version of the Forte system, including an implementation of reFLect, is freely downloadable from Intel. By Allan McInnes at 2006-12-01 05:07 | LtU Forum | previous forum topic | next forum topic | other blogs | 11653 reads
|
Browse archivesActive forum topics |
Recent comments
1 week 6 days ago
4 weeks 1 day ago
13 weeks 3 days ago
13 weeks 5 days ago
13 weeks 6 days ago
20 weeks 6 days ago
26 weeks 4 days ago
26 weeks 5 days ago
27 weeks 4 days ago
30 weeks 2 days ago