iwilare
λ(λ1(00))(λ1(00)) • モナドは単なる自己関手の圏におけるモノイド対象だよ。何か問題でも？
Tallinn University of TechnologyTallinn, Estonia
Pinned Repositories
agda-categories
A new Categories library for Agda
algebraic-temporal-logics
Semantics of counterpart-based quantified (linear) temporal logics in Agda
categorical-automata
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.org/abs/2305.00272
categorical-qtl
Categorical semantics of counterpart-based quantified (linear) temporal logics in Agda using https://github.com/agda/agda-categories
church-rosser
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 the infrastructure for λ-terms and substitutions provided by the PLFA book
dinaturality
Agda formalization for the paper "Directed equality for (co)end calculus" and its extended version.
formal-methods
Operational semantics, Type-based information flow security, Hoare logic, Verification conditions, and Separation logic in Agda for the IMP language
moirphism
solitaire
A minimal golfed web version of the MOLEK-SYNTEZ solitaire by Zachtronics
iwilare's Repositories
iwilare/church-rosser
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 the infrastructure for λ-terms and substitutions provided by the PLFA book
iwilare/categorical-automata
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.org/abs/2305.00272
iwilare/formal-methods
Operational semantics, Type-based information flow security, Hoare logic, Verification conditions, and Separation logic in Agda for the IMP language
iwilare/categorical-qtl
Categorical semantics of counterpart-based quantified (linear) temporal logics in Agda using https://github.com/agda/agda-categories
iwilare/dinaturality
Agda formalization for the paper "Directed equality for (co)end calculus" and its extended version.
iwilare/solitaire
A minimal golfed web version of the MOLEK-SYNTEZ solitaire by Zachtronics
iwilare/moirphism
iwilare/algebraic-temporal-logics
Semantics of counterpart-based quantified (linear) temporal logics in Agda
iwilare/sap-tracker
Super Auto Pets achievements tracker
iwilare/programming-in-ct
Lecture notes for the lab sessions of the "Category Theory and its Applications" course 2024 @ Tallinn University of Technology
iwilare/qltl-pnf
Positive normal forms for counterpart-based temporal logics, with a standard non-categorical semantics
iwilare/sol-lang
Sol - Simple Object Language: minimal Smalltalk-like interpreted language
iwilare/compiler-course-unipi
Project and assignments for the "Languages, Interpreters and Compilers" 2020/2021 course @ Department of Computer Science, University of Pisa https://github.com/lillo/compiler-course-unipi
iwilare/monoid-forth
Bootstrapping x86_64 operating system and minimal Forth interpreter, using UEFI
iwilare/nix
nix nix nix nix nix nix nix nix nix nix nix nix
iwilare/lis-2022
Repository for the "Laboratory for Innovative Software" project 2021/2022
iwilare/advanced-programming
Assignments for the "Advanced Programming" 2020/2021 course @ Department of Computer Science, University of Pisa http://pages.di.unipi.it/corradini/Didattica/AP-20/
iwilare/agda-categories
where the magic happens
iwilare/backgrounds
My backgrounds
iwilare/birthdays
A .csv to .ics converter for recurrent events
iwilare/chi-font
A minimal segment-based font
iwilare/dinaturality-bruteforce
https://mathoverflow.net/questions/478716/example-of-two-dinatural-transformations-between-finite-categories-that-do-not-c
iwilare/doomsday-quiz
iwilare/iwi-dejavu
iwilare/iwilare.github.io
iwilare/neovim
iwilare/numpad
Memorizing digit sequences with unlock patterns
iwilare/planets
Planetary simulation with numerical integration and PixiJS
iwilare/resolution-jumper
Utility to "visually" synchronize a mouse pointer between screens of different resolutions on Windows
iwilare/video-motion-detection
Project for the "Parallel and Distributed Systems: Paradigms and Models" 2021/2022 course @ Department of Computer Science, University of Pisa