- sequoia: a web-based tool for testing and reasoning about sequent calculi
- abella-reasoning: formalization of cut-elimination proofs (à la Gentzen) in the proof assistant Abella. Result of Leonardo Lima’s internship at Parsifal (Winter/2015).
- checkers: a proof checker based on Foundational Proof Certificates
- teyjus: contributions to the implementation of λ-prolog [OCaml, C]
- quati: online system for checking permutation of sequent calculus rules [OCaml, JQueryUI, Pyhton]
- tatu: online system for reasoning about sequent calculus specifications in linear logic with subexponentials [OCaml, JQueryUI, Python]
- gapt: generic architecture for proof transformations [Scala]
- sellf system: implementation of linear logic with subexponentials [OCaml]
- sellf and other systems in λ-Prolog (tar.gz): simple implementation of linear logic with subexponentials and the specification of some systems in it (results from the master’s degree) [λ-prolog]
Skip to content
Just another human being