Discover @iwilare Open Source projects

Andrea Laretto (@iwilare)

iwilare

Stars
78
Global Rank 248,572 (Top 9 %)
Followers 31
Following 17
Registered over 10 years ago
Most used languages

Agda 42.9 %

HTML
14.3 %

C++
14.3 %

OCaml
7.1 %

Rust
7.1 %

Java
7.1 %

Nix
7.1 %
Location 🇪🇪 Estonia
Country Total Rank 315
Country Ranking

Agda 1

OCaml
2

Nix
8

HTML
27

Rust
32

C++
122

Java
348

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

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

formal-methods

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

solitaire

A minimal golfed web version of the MOLEK-SYNTEZ solitaire by Zachtronics

categorical-qtl

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

sap-tracker

Super Auto Pets achievements tracker

algebraic-temporal-logics

Semantics of counterpart-based quantified (linear) temporal logics in Agda

factorio-planner

Simple utility to calculate quantitative dependency graphs in Factorio

qltl-pnf

Positive normal forms for counterpart-based temporal logics, with a standard non-categorical semantics

nix

nix nix nix nix nix nix nix nix nix nix nix nix

programming-in-ct

Lecture notes for the lab sessions of the "Category Theory and its Applications" course 2024 @ Tallinn University of Technology

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

CompetitiveProgramming

Assignments for the "Competitive Programming and Contests" 2020/2021 course @ Department of Computer Science, University of Pisa https://github.com/rossanoventurini/CompetitiveProgramming

sol-lang

Sol - Simple Object Language: minimal Smalltalk-like interpreted language

neural-network

A simple C++ implementation of feed forward neural networks with backpropagation, Tikhonov regularization, momentum, implementing holdout and K-fold CV