• Bar Induction is Compatible with Constructive Type Theory
    Vincent Rahli, Mark Bickford, Liron Cohen and Robert Constable
    To appear in JACM
  • A Verified Theorem Prover Backend Supported by a Monotonic Library [pdf, EasyChair]
    Vincent Rahli, Liron Cohen, Mark Bickford
    Proceedings of LPAR, 2018
  • Uniform Inductive Reasoning in Transitive Closure Logic via Infinite Descent [pdf, DROPS]
    Liron Cohen, Reuben N. S. Rowe
    Proceedings of CSL, 2018
  • Computability Beyond Church-Turing via Choice Sequences [pdf, ACM]
    Mark Bickford, Liron Cohen, Robert Constable and Vincent Rahli
    Proceedings of LICS, 2018
  • Applicable Mathematics in a Minimal Computational Theory of Sets [pdf, Episciences]
    Arnon Avron and Liron Cohen
    Journal of Logical Methods in Computer Science, 2018
  • Reasoning Inside The Box: Deduction in Herbrand Logics [pdf, EasyChair]
    Liron Cohen and Yoni Zohar
    Proceedings of GCAI, 2017
  • A Minimal Computational Theory of a Minimal Computational Universe [pdf, SpringerLink]
    Arnon Avron and Liron Cohen
    Proceedings of LFCS, 2017
  • Completeness for Ancestral Logic via a Computationally-Meaningful Semantics [pdf, SpringerLink]
    Liron Cohen
    Proceedings of TABLEAUX, 2017
  • Intuitionistic Ancestral Logic [pdf, Oxford Journals]
    Liron Cohen and Robert Constable
    Journal of Logic and Computation, 2015
  • Formalizing Scientifically Applicable Mathematics in a Definitional Framework [pdf,JFR]
    Arnon Avron and Liron Cohen
    Journal of Formalized Reasoning, 2015
  • Intuitionistic Ancestral Logic as a Dependently Typed Abstract Programming Language [pdf, SpringerLink]
    Liron Cohen and Robert Constable
    Proceedings of WoLLIC, 2015
  • The Middle Ground - Ancestral Logic [pdf, SpringerLink]
    Liron Cohen and Arnon Avron
    Synthese, 2014
  • Ancestral Logic: A Proof Theoretical Study [pdf, SpringerLink]
    Liron Cohen and Arnon Avron
    Proceedings of WoLLIC, 2014


  • Formalizing Mathematics via Predicative and Constructive Approaches [pdf]
    Ph.D. Thesis
    Tel Aviv University, 2016
  • Ancestral Logic and Equivalent Systems [pdf]
    M.Sc. Thesis
    Tel Aviv University, 2010

Presentations in International Conferences and Workshops

  • Non-well-founded Proof System for Transitive Closure Logic [abstract]
    Women in Logic Workshop, 2018
  • Cycles for Automating Induction [abstract]
    Association for Symbolic Logic North American annual meeting (invited talk), 2018
  • Extending Church Turing Computability [slides]
    Summer School on Types, Sets and Constructions (guest lecture), 2018
  • A Minimal Predicative Framework for Formalizing Mathematics [abstract]
    Association for Symbolic Logic North American annual meeting, 2017
  • Predicative Mathematics via Safety Relations [abstract]
    Logic Colloquium, 2014
  • Intuitionistic Ancestral Logic [abstract]
    Proof, Structure and Computation Workshop, Affiliated with CSL-LICS, 2014
  • Ancestral Logic [abstract]
    Between First and Second Order Logic Workshop, Unilog, 2013