Tag: Cecylia Rauszer
-
Discussing “An algebraic and Kripke-style approach to a certain extension of intuitionistic logic”
Heyting-Brouwer logic (more commonly known now as bi-intuitionistic logic) has fascinated me since I first learned of it. The idea is beguilingly simple: extend intuitionistic logic with a new connective that makes it completely symmetrical. The ‘symmetry’ I am thinking of (perhaps better called ‘duality’, but not quite the same thing as De Morgan duality)…
Categories
Recent Posts
- Discussing “Z3: An Efficient SMT Solver”
- Discussing “BI as an Assertion Language for Mutable Data Structures”
- Discussing “Sheaves in Geometry and Logic”
- Discussing “Extended Curry-Howard Correspondence for a Basic Constructive Modal Logic”
Tags
1994 1996 2000 2001 2014 2019 2020 2021 2023 Andrew W. Appel Bedrock Systems Cambridge Tracts in Theoretical Computer Science Carnegie Mellon University Christopher D. Richards City University of New York Coq Cubical Type Theory Côte d'Azur University Fabian Kunze Gregory Malecha Inria Nantes intuitionistic logic intuitionistic modal logic Jonathan Sterling Journal of Automated Reasoning LICS Matthieu Sozeau Metaprogramming modal logic Nicolas Tabareau Notre Dame Journal of Formal Logic Paul-André Melliès POPL Princeton University Proof theory Rocq Saarland University Théo Winterhalter types type theory University of Amsterdam University of Birmingham University of Cambridge University of Oxford Valeria de Paiva