ICFP 2020 (series) / TyDe 2020 (series) / TyDe 2020 /
Predictable Macros for Hindley-Milner (Extended Abstract)
We present “Klister”, an ML-like language with hygienic type-driven macros that have a predictable yet procedural programming model. Klister’s macros are hygienic in that they prevent variable capture by default, and they are type-driven in that macros have access to the type that is expected for the expression that is to be produced. Being procedural means that macros are written in the full Klister language, rather than a restricted subset in the style of Scheme’s syntax-rules
, and predictable means that macro developers can be blissfully unaware of the type checker’s implementation details, in particular the order in which it traverses expressions.
Sun 23 AugDisplayed time zone: Eastern Time (US & Canada) change
Sun 23 Aug
Displayed time zone: Eastern Time (US & Canada) change
15:30 - 17:00 | |||
15:30 30mTalk | Predictable Macros for Hindley-Milner (Extended Abstract) TyDe | ||
16:00 30mTalk | Strongly Bounded Termination with Applications to Security and Hardware Synthesis TyDe Thomas Reynolds University of Missouri, William Harrison Oak Ridge National Laboratory, Rohit Chadha University of Missouri, Gerard Allwein U.S. Naval Research Laboratory | ||
16:30 30mTalk | Developing a Dependently Typed Language with Runtime Proof Search (Extended Abstract) TyDe |