sacerdot Goto Github PK

causal2timedformalization

Sources for the formalization in Matita of Causal Reversibility Implies Time Reversibility

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.

coqine

A Coq plugin to translate Coq proofs into Dedukti terms.

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.

dedukti

Implementation of the λΠ-calculus modulo rewriting

emerging2223project

Emerging Programming Languages 20223/2023 Project Specification

europroofnet.github.io

Sources of the EuroProofNet web site.

functionsasprocesses

Sources for the formalization in Abella of Functions (lambda-calculus) as Processes (pi-calculus)

lambdapi

Proof assistant based on the λΠ-calculus modulo rewriting

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

mttinabella

A formalization of MTT in Abella

ocaml-expat

The official repository of the ocaml-expat library

ocaml-http

opam-repository

Main public package repository for OPAM, the source package manager of OCaml.

scam

The implementation of the Strong Crumbling Abstract Machine (SCAM) for the Strong Call-by-value lambda-calculus (see paper at LICS 2021)

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

smartanalysis

Academic code to check smart contract properties

theoremprover-museum.github.io

ulex