Pinned

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 18 1

2. categorical-automata categorical-automata Public

   Bicategories of automata, completeness of F-automata in monoidal categories, adjoints between (semi)bicategories; https://arxiv.org/pdf/2303.03867, https://arxiv.org/pdf/2303.03865, https://arxiv.o…

   Agda 15 1

3. 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 12

4. categorical-qtl categorical-qtl Public

   Categorical semantics of counterpart-based quantified (linear) temporal logics in Agda using https://github.com/agda/agda-categories

   Agda 6

5. agda/agda-categories agda/agda-categories Public

   A new Categories library for Agda

   Agda 347 64

6. lambda.js lambda.js

   1

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