kirancodes.me
To Proof Maintenance & Beyond!

Programmable semantic fragments: the design and implementation of typy

Cyrus Omar, Jonathan Aldrich

Abstract

This paper introduces typy, a statically typed programming language embedded by reflection into Python. typy features a fragmentary semantics, i.e. it delegates semantic control over each term, drawn from Python's fixed concrete and abstract syntax, to some contextually relevant user-defined semantic fragment. The delegated fragment programmatically 1) typechecks the term (following a bidirectional protocol); and 2) assigns dynamic meaning to the term by computing a translation to Python.

Related papers