Papers
A Rig of Transformations
In high-level functional languages, the compiler often gives users little control over the runtime representation of data types. Yet how we model data structures at the program level can be different to how we want to represent them at the binary level, for efficiency or legacy reasons. Hence being able to describe data layouts and their transformations for data types is a useful and necessary part of programming, but difficult to do correctly, efficiently and ergonomically. We present a model of finite algebraic data types as a commutative rig (a ring without additive inverses), where the rig-equalities are modelled by isomorphisms between data. Using this approach, we can also model embedding a data type into a larger type (e.g. bit-padding) as a partial isomorphism.
Classical Call by Push Value
Call by Push Value (CBPV) is a calculus for explicitly modelling call-by-name and call-by-value reduction in the λ-calculus and many other intuitionistic logic-based calculi. We investigate whether classical logic-based calculi, specifically the λ̅μμ̃-calculus, can model CBPV and therefore subsume the call-by-name and call-by-value paradigms. We augment the λ̅μμ̃-calculus syntax with new features inspired by CBPV, and provide a translation from CBPV into the augmented λ̅μμ̃-calculus. By limiting the traditional reduction of λ̅μμ̃, we can simulate CBPV reduction in this augmented calculus. This should open up avenues for describing the semantics of call-by-name and call-by-value via classical logic semantics.