-
Tallinn University of Technology
- Tallinn, Estonia
-
02:35
- 3h ahead - iwilare.com
- @iwilare
- @iwilare@types.pl
Highlights
Pinned Loading
-
church-rosser
church-rosser PublicA 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…
-
formal-methods
formal-methods PublicOperational semantics, Type-based information flow security, Hoare logic, Verification conditions, and Separation logic in Agda for the IMP language
-
categorical-qtl
categorical-qtl PublicCategorical semantics of counterpart-based quantified (linear) temporal logics in Agda using agda-categories
Agda 7
-
dinaturality
dinaturality PublicAgda formalization for the preprint "Directed equality with dinaturality".
Agda 8
-
category-theory-course-2025
category-theory-course-2025 PublicLecture notes for the "Introduction to Category Theory and its Applications" course 2025 (Track B - Computer Science) @ Tallinn University of Technology
-
lambda.js
lambda.js 1E=([a,b],Γ=[])=>b?a?E(a,Γ)(E(b,Γ)):x=>E(b,[x,...Γ]):Γ[a]
437 contributions in the last year
Day of Week | April Apr | May May | June Jun | July Jul | August Aug | September Sep | October Oct | November Nov | December Dec | January Jan | February Feb | March Mar | |||||||||||||||||||||||||||||||||||||||||
Sunday Sun | |||||||||||||||||||||||||||||||||||||||||||||||||||||
Monday Mon | |||||||||||||||||||||||||||||||||||||||||||||||||||||
Tuesday Tue | |||||||||||||||||||||||||||||||||||||||||||||||||||||
Wednesday Wed | |||||||||||||||||||||||||||||||||||||||||||||||||||||
Thursday Thu | |||||||||||||||||||||||||||||||||||||||||||||||||||||
Friday Fri | |||||||||||||||||||||||||||||||||||||||||||||||||||||
Saturday Sat |