Pinned Loading

1. church-rosser church-rosser Public

   A complete proof in Agda of the Church-Rosser theorem for untyped λ-calculus formalizing the methods by Komori-Matsuda-Yamakawa (2014) and the proof by Nagele-van Oostrom-Sternagel (2016); reuses t…

   Agda 29 1

2. formal-methods formal-methods Public

   Operational semantics, Type-based information flow security, Hoare logic, Verification conditions, and Separation logic in Agda for the IMP language

   Agda 19

3. categorical-qtl categorical-qtl Public

   Categorical semantics of counterpart-based quantified (linear) temporal logics in Agda using agda-categories

   Agda 8

4. dinaturality dinaturality Public

   Agda formalization for the POPL 2026 paper "Di- is for Directed: First-Order Directed Type Theory via Dinaturality".

   Agda 8

5. category-theory-course-2025 category-theory-course-2025 Public

   Lecture notes for the "Introduction to Category Theory and its Applications" course 2025 (Track B - Computer Science) @ Tallinn University of Technology

   5 1

6. lambda.js lambda.js

   1

   E=([a,b],Γ=[])=>b?a?E(a,Γ)(E(b,Γ)):x=>E(b,[x,...Γ]):Γ[a]