Projects

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