Ancestral Logic: A Proof Theoretical Study. - Liron Cohen 001; Arnon Avron (WoLLIC, 2014)

Intuitionistic Ancestral Logic as a Dependently Typed Abstract Programming Language. - Liron Cohen 001; Robert L. Constable (WoLLIC, 2015)

Formalizing Scientifically Applicable Mathematics in a Definitional Framework. - Arnon Avron; Liron Cohen 001 (J. Formaliz. Reason., 2016)

Reasoning Inside The Box: Deduction in Herbrand Logics. - Liron Cohen 001; Yoni Zohar (GCAI, 2017)

Completeness for Ancestral Logic via a Computationally-Meaningful Semantics. - Liron Cohen 001 (TABLEAUX, 2017)

Uniform Inductive Reasoning in Transitive Closure Logic via Infinite Descent. - Liron Cohen 001; Reuben N. S. Rowe (CSL, 2018)

A Minimal Computational Theory of a Minimal Computational Universe. - Arnon Avron; Liron Cohen 001 (LFCS, 2018)

Computability Beyond Church-Turing via Choice Sequences. - Mark Bickford; Liron Cohen 001; Robert L. Constable; Vincent Rahli (LICS, 2018)

A Verified Theorem Prover Backend Supported by a Monotonic Library. - Vincent Rahli; Liron Cohen 001; Mark Bickford (LPAR, 2018)

Infinitary and Cyclic Proof Systems for Transitive Closure Logic. - Liron Cohen 001; Reuben N. S. Rowe (CoRR, 2018)

Applicable Mathematics in a Minimal Computational Theory of Sets. - Arnon Avron; Liron Cohen 001 (Log. Methods Comput. Sci., 2018)

The Effects of Effects on Constructivism. - Liron Cohen 001; Sofia Abreu Faro; Ross Tate (MFPS, 2019)

Bar Induction is Compatible with Constructive Type Theory. - Vincent Rahli; Mark Bickford; Liron Cohen 001; Robert L. Constable (J. ACM, 2019)

Towards automated reasoning in Herbrand structures. - Liron Cohen 001; Reuben N. S. Rowe; Yoni Zohar (J. Log. Comput., 2019)

Intuitionistic ancestral logic. - Liron Cohen 001; Robert L. Constable (J. Log. Comput., 2019)

The middle ground-ancestral logic. - Liron Cohen 001; Arnon Avron (Synth., 2019)

Integrating Induction and Coinduction via Closure Operators and Proof Cycles. - Liron Cohen 001; Reuben N. S. Rowe (IJCAR (1), 2020)

Non-well-founded Proof Theory of Transitive Closure Logic. - Liron Cohen 001; Reuben N. S. Rowe (ACM Trans. Comput. Log., 2020)

Non-well-founded Deduction for Induction and Coinduction. - Liron Cohen 001 (CADE, 2021)

Formally Computing with the Non-computable. - Liron Cohen 001 (CiE, 2021)

Open Bar - a Brouwerian Intuitionistic Logic with a Pinch of Excluded Middle. - Mark Bickford; Liron Cohen 001; Robert L. Constable; Vincent Rahli (CSL, 2021)

Evidenced Frames: A Unifying Framework Broadening Realizability Models. - Liron Cohen 001; Étienne Miquey; Ross Tate (LICS, 2021)

Constructing Unprejudiced Extensional Type Theories with Choices via Modalities. - Liron Cohen 001; Vincent Rahli (FSCD, 2022)

A geometric method for improved uncertainty estimation in real-time. - Gabriella Chouraqui; Liron Cohen 001; Gil Einziger; Liel Leman (UAI, 2022)

Realizing Continuity Using Stateful Computations. - Liron Cohen 001; Vincent Rahli (CSL, 2023)

Inductive Continuity via Brouwer Trees. - Liron Cohen 001; Bruno da Rocha Paiva; Vincent Rahli; Ayberk Tosun (MFCS, 2023)

Uncertainty Estimation based on Geometric Separation. - Gabriella Chouraqui; Liron Cohen 001; Gil Einziger; Liel Leman (CoRR, 2023)

TT☐C: a Family of Extensional Type Theories with Effectful Realizers of Continuity. - Liron Cohen 001; Vincent Rahli (CoRR, 2023)

Separating Markov's Principles. - Liron Cohen 001; Yannick Forster 002; Dominik Kirst; Bruno da Rocha Paiva; Vincent Rahli (LICS, 2024)

$ text{TT}^{ Box}_{ mathcal C}$: a Family of Extensional Type Theories with Effectful Realizers of Continuity. - Liron Cohen 001; Vincent Rahli (Log. Methods Comput. Sci., 2024)

The Complex(ity) Landscape of Checking Infinite Descent. - Liron Cohen 001; Adham Jabarin; Andrei Popescu 001; Reuben N. S. Rowe (Proc. ACM Program. Lang., 2024)

Computation First: Rebuilding Constructivism with Effects (Invited Talk). - Liron Cohen 001 (FSCD, 2025)

From Partial to Monadic: Combinatory Algebra with Effects. - Liron Cohen 001; Ariel Grunfeld; Dominik Kirst; Étienne Miquey (FSCD, 2025)

Cyclone: A Heterogeneous Tool for Verifying Infinite Descent. - Liron Cohen 001; Reuben N. S. Rowe; Matan Shaked (TACAS (1), 2025)

Syntactic Effectful Realizability in Higher-Order Logic. - Liron Cohen 001; Ariel Grunfeld; Dominik Kirst; Étienne Miquey (CoRR, 2025)