Pinned Repositories
Causal2TimedFormalization
Sources for the formalization in Matita of Causal Reversibility Implies Time Reversibility
CovidMonitoring
A small project in Erlang to pass the exam of Emerging Programming Paradigms @ University of Bologna
Crumbling-Abstract-Machines
This repository contains the formalization of part of the theory behind the Crumbling Abstract Machines, that has been introduced and partially developed in Beniamino Accattoli, Andrea Condoluci, Giulio Guerrieri, and Claudio Sacerdoti Coen. 2019. Crumbling Abstract Machines. In Proceedings of ACM Conference (Conference’17). ACM, New York, NY,USA,39 pages.
Emerging2223Project
Emerging Programming Languages 20223/2023 Project Specification
matita
An Interactive Theorem Prover for a variant of the Calculus of (Co)Inductive Constructions
matita-lean
Porting of Matita's declarative syntax to Lean
MiniErlangBlockchain
Homework: a mini-blockchain implementation in Erlang
Minimalist-Type-Theory-In-Lambda-Prolog
An implementation in Lambda-Prolog of the Minimalist Type Theory
ocaml-http
sesame
Implementation in OCaml of a strong reduction machine for Intuitionistic Multiplicative Exponential Linear Logic (IMELL) that has linear overhead on the number of reduction steps and the size of the initial term
sacerdot's Repositories
sacerdot/ocaml-http
sacerdot/MiniErlangBlockchain
Homework: a mini-blockchain implementation in Erlang
sacerdot/CovidMonitoring
A small project in Erlang to pass the exam of Emerging Programming Paradigms @ University of Bologna
sacerdot/matita
An Interactive Theorem Prover for a variant of the Calculus of (Co)Inductive Constructions
sacerdot/Minimalist-Type-Theory-In-Lambda-Prolog
An implementation in Lambda-Prolog of the Minimalist Type Theory
sacerdot/Emerging2223Project
Emerging Programming Languages 20223/2023 Project Specification
sacerdot/Crumbling-Abstract-Machines
This repository contains the formalization of part of the theory behind the Crumbling Abstract Machines, that has been introduced and partially developed in Beniamino Accattoli, Andrea Condoluci, Giulio Guerrieri, and Claudio Sacerdoti Coen. 2019. Crumbling Abstract Machines. In Proceedings of ACM Conference (Conference’17). ACM, New York, NY,USA,39 pages.
sacerdot/matita-lean
Porting of Matita's declarative syntax to Lean
sacerdot/SCAM
The implementation of the Strong Crumbling Abstract Machine (SCAM) for the Strong Call-by-value lambda-calculus (see paper at LICS 2021)
sacerdot/sesame
Implementation in OCaml of a strong reduction machine for Intuitionistic Multiplicative Exponential Linear Logic (IMELL) that has linear overhead on the number of reduction steps and the size of the initial term
sacerdot/Causal2TimedFormalization
Sources for the formalization in Matita of Causal Reversibility Implies Time Reversibility
sacerdot/coq
Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.
sacerdot/CoqInE
A Coq plugin to translate Coq proofs into Dedukti terms.
sacerdot/Dedukti
Implementation of the λΠ-calculus modulo rewriting
sacerdot/ocaml-expat
The official repository of the ocaml-expat library
sacerdot/europroofnet.github.io
Sources of the EuroProofNet web site.
sacerdot/FunctionsAsProcesses
Sources for the formalization in Abella of Functions (lambda-calculus) as Processes (pi-calculus)
sacerdot/lambdapi
Proof assistant based on the λΠ-calculus modulo rewriting
sacerdot/MTTinAbella
A formalization of MTT in Abella
sacerdot/opam-repository
Main public package repository for OPAM, the source package manager of OCaml.
sacerdot/SmartAnalysis
Academic code to check smart contract properties
sacerdot/theoremprover-museum.github.io
sacerdot/ulex