Skip to content
View iwilare's full-sized avatar
🌌
🌌

Block or report iwilare

Block user

Prevent this user from interacting with your repositories and sending you notifications. Learn more about blocking users.

You must be logged in to block users.

Please don't include any personal information such as legal names or email addresses. Maximum 100 characters, markdown supported. This note will be visible to only you.
Report abuse

Contact GitHub support about this user’s behavior. Learn more about reporting abuse.

Report abuse

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 23 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 15 1

  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 367 68

  6. lambda.js lambda.js
    1
    E=([a,b],Γ=[])=>b?a?E(a,Γ)(E(b,Γ)):x=>E(b,[x,...Γ]):Γ[a]