A Dependent Language with Type-Safe Program Extraction
Program extraction for dependently-typed languages such as Rocq often requires unsafe type casts. In this work I present some early ideas on a language called Extractly. To remove type-casts from extracted Extractly programs, we forbid large elimination of data types and rely on indexed data types (GADTs). Whilst nothing has yet been formalised, I present a "recipe" for removing large elimination which works for all examples I have found. This includes a metacircular interpreter for the simply-typed lambda calculus.
A Dependent Language with Type-Safe Program Extraction
Program extraction for dependently-typed languages such as Rocq often requires unsafe type casts. In this work in progress I introduce Extractly, a first-order language with data types and codata types inspired by Binder et. al.’s Polarity. Restrictions on large elimination help remove the dependence of types on terms, whilst changes to well-formedness checking of data types ensure little-to-no loss in expressivity.
A Fuelled Self-Reducer for System T
Self-reducers are programs that reduce embeddings of expressions to thier normal forms. They are written in the same language that they reduce. To date, there are no self-reducers for strongly-normalising languages. I have implemented a fuelled self-reducer for System T. Rather than working with Gödel encodings, I used Kiselyov's and Longley and Normalnn's encodings for structured types such as products, sums, and some inductive types. Working with these types within System T produces large unreadable terms. I promote these structured types to first class features of a new metalanguage called Primrose. Primrose compiles into System T. Work on Primrose is ongoing.
Freely Extending Interpreters
A partial evaluator extends an interpreter to work on terms with free variables. In this talk, I will formalise this intuition for pure simply-typed languages. I will focus on the simply-typed lambda calculus, but my definitions are in terms of any second-order algebra as defined by Fiore. After giving a definition for a denotational interpreter, I will define what it means for a model of a language (formulated as a SOAS algebra) to extend an interpreter, as well as morphisms between extensions. From this, I will define the free extension of an interpreter, which is the least opinionated partial evaluator.