Danil Annenkov

two-level. Two-Level Type Theory

unmix. A simple program specializer (based on partial evaluation) for a subset of Scheme. It includes a binding time analyzer, a residual program generator and an arity raiser.

trace-monoids. Trace monoids in Cubical Agda

contracts. Symbolic financial contract EDSL

futhark-extract. Extracting Futhark code from the Coq proof assistant

stratego-sll. An interpreter and minimal supercompiler for simple lazy language (first-order functional language) written in Stratego transformation language (Spoofax language workbench).

concordium-marlowe. Marlowe interpreter and contract manager

stlcnorm. Simply-typed lambda calculus and extensions: termination, extrinsic/intrinsic representations, nominal binding techniques

LBS. Supplementary materials for the Language-based Security Lecture on Smart Contracts

sql-dsl. Racket