- sml-to-coq: a tool that translates SML code into Coq, and SML contracts into Coq theorems (with Laila El-beheiry and Ammar Karkour)
- sequoia: a web-based tool for testing and reasoning about sequent calculi (with Abdulrahman Alfayad, Zan Naeem, and Mohammed Hashim)
- abella-reasoning: formalization of cut-elimination proofs (à la Gentzen) in the proof assistant Abella (with Kaustuv Chaudhuri and Leonardo Lima). Result of Leonardo Lima’s internship at Parsifal (Winter/2015).
- checkers: a proof checker based on Foundational Proof Certificates (with Tomer Libal)
- quati: online system for checking permutation of sequent calculus rules (with Leonardo Lima and Vivek Nigam) [OCaml, JQueryUI, Pyhton]
- tatu: online system for reasoning about sequent calculus specifications in linear logic with subexponentials (with Vivek Nigam and Elaine Pimentel) [OCaml, JQueryUI, Python]
- gapt: generic architecture for proof transformations (with lots of colleagues) [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