Write a Blog >>
SPLASH 2017
Sun 22 - Fri 27 October 2017 Vancouver, Canada
Sun 22 Oct 2017 15:52 - 16:15 at Regency A - Session 4 Chair(s): Lindsey Kuper

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

Displayed time zone: Tijuana, Baja California change

15:30 - 17:00
Session 4DSLDI at Regency A
Chair(s): Lindsey Kuper Intel Labs
15:30
22m
Talk
Property Law as a Programming Language
DSLDI
Shrutarshi Basu Cornell University, James Grimmelmann Cornell Law School, Nate Foster Cornell University
File Attached
15:52
22m
Talk
Embedding By Normalisation
DSLDI
Shayan Najd University of Edinburgh
File Attached
16:15
22m
Talk
Reliable composition of domain-specific language features
DSLDI
Ted Kaminski University of Minnesota, Eric Van Wyk University of Minnesota, USA
File Attached
16:37
22m
Day closing
Discussion and closing remarks
DSLDI