Title
A reflective functional language for hardware design and theorem proving
Abstract
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. The paper motivates and presents the syntax and type system of this language, which brings together a new combination of pattern-matching and reflection features targeted specifically at our application domain. It also gives an operational semantics based on a novel use of contexts as expression constructors, and it presents a scheme for compiling reFLect programs using the same context mechanism.
Year
DOI
Venue
2006
10.1017/S0956796805005757
J. Funct. Program.
Keywords
Field
DocType
theorem proving,application domain,reflect program,reflect language,paper motivates,hardware design,expression constructor,decompose expression,context mechanism,antiquotation construct,reflective functional language,functional programming language,operational semantics,type system,pattern matching,functional language
Specification language,Programming language,Programming language specification,Computer science,Language construct,Theoretical computer science,Object language,High-level programming language,Computer hardware,Low-level programming language,Programming language implementation,Language primitive
Journal
Volume
Issue
ISSN
16
2
0956-7968
Citations 
PageRank 
References 
28
1.31
23
Authors
3
Name
Order
Citations
PageRank
Jim Grundy117918.11
Thomas F. Melham238435.63
John O'leary3281.31