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 | 12285 reads
|
Browse archives
Active forum topics |
Recent comments
16 weeks 5 days ago
16 weeks 6 days ago
16 weeks 6 days ago
39 weeks 8 hours ago
43 weeks 2 days ago
44 weeks 6 days ago
44 weeks 6 days ago
47 weeks 4 days ago
1 year 16 hours ago
1 year 17 hours ago