⌂ Home

# Projects

Ldmc — The Ladder-Typed Data Morphing Compiler

Given a description of input/output types, ldmc generates code for transforming between different data representations of the same abstract type....

Ltsh — A Type Checker for the Unix Shell

Ltsh is a tiny utility program for type-analysis of shell pipelines based on ladder types....

Combwriter

Ergonomical split-typewriter with fully 3D-Printed Circuit Board. Through its unique hexagonally shaped keycaps, the layout naturally follows an ergonomic V shape to fit the different lengths of the fingers....

# Articles

Type Systems

Representation Bugs with Typed Languages

In many systems, critical semantic distinctions exist only in the minds of programmers. For example, take the following C code from gpsutils.c of the gpsd project[1]...

Compatibility via Conversion (Coercive Subtyping)

Implicit type conversion functions, also known as coercions, provide an alternative approach to implement subtyping. Instead of interpreting subtyping as set inclusion (where the values of one type are contained within another), a coercive subtype system regards two types as compatible if there exists a conversion function between them. In this...

(In-)Coherence under Transitivity of Coercive Subtyping

While coercions improve ergonomics, the freedom to add them introduces the risk of inconsistency. In particular, multiple coercion paths between the same two types may produce different results. Example 6. Suppose we have the following coercions, which would prove quite useful for pretty printing and serialization:...

Types in the Context of Distributed Systems

Type systems generally assume a fixed representation of values within a single platform. With this design, they achieve to provide a safe island of abstraction for computation on one machine, where values can be stored, manipulated, and passed between functions....