Using Bars to Push the Limits of Computability Mark Bickford, Liron Cohen, Robert L. Constable and Vincent Rahli
Journal of the ACM, 2026 (to appear)
Sheaf Realizability for Dependent Type Theory Bruno da Rocha Paiva, Vincent Rahli, Sam Speight and Liron Cohen
Proceedings of CSL, 2027 (to appear)
Semantic Geometric Calibration in Randomized Neural Feature Space [pdf, IJCAI]
Itay Abuhazera, Liron Cohen and Gil Einziger
Proceedings of IJCAI, 2026
Evidence-Tracked Tape Semantics for Probabilistic Computation [ArXiv,DROPS]
Liron Cohen and Tomer Samara
Proceedings of FSCD, 2026
Multicategorical Semantics for Untyped Effects [ArXiv]
Liron Cohen and Ariel Grunfeld
Proceedings of MFPS, 2026
Certified Infinite Descent Criteria in Isabelle/HOL [pdf,DROPS]
Jamie Wright, Liron Cohen, Andrei Popescu and Reuben N. S. Rowe
Proceedings of ITP, 2026
Syntactic Effectful Realizability in Higher-Order Logic [pdf,IEEE]
Liron Cohen, Ariel Grunfeld, Dominik Kirst and Étienne Miquey
Proceedings of LICS, 2025
Computation First: Rebuilding Constructivism with Effects [pdf,DROPS]
Liron Cohen
Proceedings of FSCD, 2025
From Partial to Monadic: Combinatory Algebra with Effects [pdf,DROPS]
Liron Cohen, Ariel Grunfeld, Dominik Kirst and Étienne Miquey
Proceedings of FSCD, 2025
Cyclone: A Heterogeneous Tool for Verifying Infinite Descent [pdf,SpringerLink,Cyclone verifier]
Liron Cohen, Reuben Rowe and Matan Shaked
ETAPS Distinguished Paper Award and Distinguished Artifact Award Proceedings of TACAS, 2025
Separating Markov's Principles [pdf,ACM]
Liron Cohen, Yannick Forster, Dominik Kirst, Bruno da Rocha Paiva and Vincent Rahli
Proceedings of LICS, 2024
BoxTT: a Family of Extensional Type Theories with Effectful Realizers of Continuity [pdf, EPISciences ]
Liron Cohen and Vincent Rahli
Logical Methods In Computer Science, 2024
The Complex(ity) Landscape of Checking Infinite Descent [pdf,ACM]
Liron Cohen, Adham Jabarin, Andrei Popescu and Reuben N. S. Rowe
Proceedings of POPL, 2024
Inductive Continuity via Brouwer Trees [pdf,DROPS]
Liron Cohen, Bruno da Rocha Paiva, Vincent Rahli, and Ayberk Tosun
Proceedings of MFCS, 2023
Monadic Realizability for Intuitionistic Higher-Order Logic [pdf]
Liron Cohen, Ariel Grunfeld and Ross Tate
Proceedings of TYPES, 2023
Realizing Continuity Using Stateful Computations
[pdf,DROPS]
Liron Cohen and Vincent Rahli
Proceedings of CSL, 2023
A Geometric Method for Improved Uncertainty Estimation in Real-time [pdf,OpenReview]
Gabriella Chouraqui, Liron Cohen, Gil Einziger and Liel Leman
Proceedings of UAI, 2022
Constructing Unprejudiced Extensional Type Theories with Choices via Modalities [pdf,DROPS]
Liron Cohen and Vincent Rahli
Proceedings of FSCD, 2022
BioTT: a Family of Brouwerian Intuitionistic Theories Open to Classical Reasoning [pdf]
Mark Bickford, Liron Cohen, Robert Constable and Vincent Rahli
Proceedings of TYPES, 2022
Evidenced Frames: A Unifying Framework Broadening Realizability Models [pdf, ACM, Coq formalization]
Liron Cohen, Etienne Miquey and Ross Tate
Proceedings of LICS, 2021
Non-well-founded Deduction for Induction and Coinduction [pdf, SpringerLink]
Liron Cohen
Proceedings of CADE, 2021
Formally Computing with the Non-computable [pdf, SpringerLink]
Liron Cohen
Proceedings of CiE, 2021
Non-well-founded Proof Theory of Transitive Closure Logic [pdf, ACM]
Liron Cohen, Reuben N. S. Rowe
Transactions on Computational Logic, 2020
Open Bar --- a Brouwerian Intuitionistic Logic with a Pinch of Excluded Middle [pdf, DROPS]
Mark Bickford, Liron Cohen, Robert Constable and Vincent Rahli
Proceedings of CSL, 2020
Integrating Induction and Coinduction via Closure Operators and Proof Cycles [pdf, SpringerLink]
Liron Cohen, Reuben N. S. Rowe
Proceedings of IJCAR, 2020
The Effects of Effects on Constructivism [pdf, ENTCS]
Liron Cohen, Sofia Abreu Faro and Ross Tate
Proceedings of MFPS, 2019
Towards Automated Reasoning in Herbrand Structures [pdf, Oxford Journals]
Liron Cohen, Reuben N. S. Rowe and Yoni Zohar
Journal of Logic and Computation, 2019
Bar Induction is Compatible with Constructive Type Theory [pdf, ACM]
Vincent Rahli, Mark Bickford, Liron Cohen and Robert Constable
Journal of the ACM, 2019
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
Manuscripts
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
