Welcome to the Types and Programming Languages (TAPL) project implemented in Coq/Rocq. This project covers the formalization of type systems and operational semantics.

Modules

Programming Language Foundations
Core chapters including Hoare Logic, Smallstep Semantics, STLC (Simply Typed Lambda Calculus) and its properties.
Browse PLF →
Properties
Auxiliary properties and relations used throughout the project development.
Browse Props →
Tactics
Custom Coq tactics and automation scripts to simplify proofs.
Browse Tactics →
Source Definitions
Base definitions for Arithmetic Expressions and other core language features.
Browse Source →
Generated on using Coqdoc and Rocq.