In this talk, we present the insight that the practical concept of embedded domain-specific compilers (EDSC), describing embedded domain-specific languages (EDSL) used for generating code often for external targets, is deeply related to the theoretical concept of Normalisation-By-Evaluation (NBE), describing the process of deriving the canonical form of terms with respect to an equational theory. Since an embedded term is encoded as a collection of host language terms, evaluation of the non-value host terms results in normalisation of the embedded term, and since EDSCs rely on an intermediate interface to generate their target code from, all embedded terms are designed to eventually adhere to the normal forms described by the interface. In other words, the structure of an EDSC allows it to perform normalisation on embedded terms by encoding them as a collection of value and non-value host terms, employing evaluation in the host language, and then deriving the resulting terms adhering to the intermediate interface. This structure, together with a collection of correctness laws, forms an NBE process. This connection, referred to as embedding by normalisation (EBN), is theoretically useful in that it helps us to understand and reason about embedded terms and their semantics, and practically beneficial in that it enables us to directly apply techniques from NBE. For instance, through EBN, we adapt the treatment of sums, or constants, from NBE to embedding, resolving some not fully resolved problems.
Sun 22 Oct
|15:30 - 15:52|
Shrutarshi BasuCornell University, James GrimmelmannCornell Law School, Nate FosterCornell UniversityFile Attached
|15:52 - 16:15|
Shayan NajdUniversity of EdinburghFile Attached
|16:15 - 16:37|
|16:37 - 17:00|