Jeremy G. Siek

deduce. A proof checker meant for education. Primarily for teaching proofs of correctness of functional programs.

abstract-binding-trees. Abstract binding trees (abstract syntax trees plus binders), as a library in Agda

B629-denotational. Topics in Programming Languages: Denotational Semantics, Spring 2018 Course at Indiana University

gradual-typing-in-agda. Formalizations of Gradually Typed Languages in Agda

B522-PL-Foundations. Course Webpage for B522 Programming Language Foundations, Spring 2020, Indiana University

featherweight-C. Featherweight C, Executable Semantics: Parser, Type Checker, and Abstract Machine

denotational_semantics. Denotational semantics based on graph and filter models

arete. Arete is an experimental programming language.

AI-for-pl. experiments in using AI to do PL metatheory

step-indexed-logic. A modal logic for reasoning about step-indexed logical relations

correct_compilers. Experiments in proving compiler correctness

al. Al: a language for teaching algorithms and data structures

B505-algorithms-public. Public material for the course B505 Applies Algorithms at Indiana University

Compilers-HW. Compilers Homework repo

prototypes-in-python. Prototypes of programming languages written in Python.

PLFA-Spring-2026. Course web page for B629 Mechanized Proofs for PL Metatheory

home. Web Page

fractional-permissions. A lambda calculus of fractional permissions

agda-stdlib-doc.