Stephanie Weirich

pi-forall. A demo implementation of a simple dependently-typed language

dth. Examples of Dependently-typed programs in Haskell

tal. An implementation of Typed Assembly Language (Morrisett, Walker, Crary, Glew)

lambda-n-ways. Benchmarks for capture-avoiding substitution

challenge. Strongly-typed System F in Haskell

corespec. A Specification for Dependent Types in Haskell (Core)

trellys. Automatically exported from code.google.com/p/trellys

replib. Replib: generic programming & Unbound: generic treatment of binders

rebound. # A simple variable binding library based on well-scoped indices and environments

lennart-lambda. λλλλ Lennart Augustsson's λ-calculus cooked four ways

hs-inferno. Generic unification-based type inference library

graded-haskell. Graded Dependent Type systems

haskelltester. Simple autograder for Haskell programming assignments

lambda-calculus. Denotational Semantics of the Untyped Lambda Calculus

pl-semantics-and-types. CIS 7000-01 Fall 2025 Course materials

equations-ln. Coq

system-fc-coq. TeX

RISCV-ISA-Spec. Formal specification of RISC-V Instruction Set

PHICWIC2018. Formal logic and software verification using interactive theorem provers

corespec-roles. Dependent Haskell with role annotations (ICFP 2019)

saw-core-what4. SAWCore backend for What4

jvm-parser. A Haskell parser for JVM bytecode files

sweirich.github.io. HTML