Projects

  • 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]