iwilare/church-rosser iwilare/church-rosser

  • Stars
    star
    18
  • Rank 1,208,065 (Top 24 %)
  • Language Agda
  • License
    MIT License
  • Created over 4 years ago
  • Updated about 2 years ago
Twitter logo Share LinkedIn logo Share Facebook logo Share
iwilare/church-rosser
github

iwilare

Reviews

There are no reviews yet. Be the first to send feedback to the community and the maintainers!

Repository Details

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

More Repositories

1

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
Agda
15
star
2

formal-methods

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

solitaire

A minimal golfed web version of the MOLEK-SYNTEZ solitaire by Zachtronics
HTML
6
star
4

categorical-qtl

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

sap-tracker

Super Auto Pets achievements tracker
HTML
3
star
6

algebraic-temporal-logics

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

factorio-planner

Simple utility to calculate quantitative dependency graphs in Factorio
Rust
2
star
8

qltl-pnf

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

nix

nix nix nix nix nix nix nix nix nix nix nix nix
Nix
1
star
10

programming-in-ct

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

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
OCaml
1
star
12

CompetitiveProgramming

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

sol-lang

Sol - Simple Object Language: minimal Smalltalk-like interpreted language
Java
1
star
14

neural-network

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