Tag: University of Birmingham
-
Discussing “Extended Curry-Howard Correspondence for a Basic Constructive Modal Logic”
This is one of the classic papers – I’ve read, and cited, it a few times over the years myself – looking at extending the classic ‘Curry-Howard’ correspondence between lambda calculus and intuitionistic logic, to intuitionistic modal logic.
-
Discussing “On Intuitionistic Diamonds (and Lack Thereof)”
I choose papers for this blog by looking at the most cited papers in my Google Scholar recommendations of recent papers. This week, my algorithm has read my mind by recommending a fairly new paper that was already at the top of my list of papers to read. Its topic, as with a few papers…
-
Discussing “Computational Types from a Logical Perspective”
This is a sequel to a paper by Moggi that I discussed some time ago. That paper discussed side effects, which are, roughly speaking, anything interesting that a program does other than map inputs deterministically to outputs, such as failure to terminate with a value, taking in user input, or producing output before the computation…
-
Discussing “Domain Theory”
Domains are certain forms of ordered sets used to address problems in the denotational semantics (mathematical interpretation) of programming languages. The area was invented by Dana Scott in a series of papers starting in 1969, building on earlier work by many others that used lattices. This book (which admittedly, I did not have time to…
Categories
Recent Posts
- Discussing “A semantics for concurrent separation logic”
- Discussing “Z3: An Efficient SMT Solver”
- Discussing “BI as an Assertion Language for Mutable Data Structures”
- Discussing “Sheaves in Geometry and Logic”
Tags
1994 1996 2000 2001 2007 2014 2019 2021 2023 Abhishek Anand 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 Cyril Cohen Côte d'Azur University Inria Nantes INRIA Rocquencourt intuitionistic logic intuitionistic modal logic Journal of Automated Reasoning LICS Matthieu Sozeau Metaprogramming modal logic Notre Dame Journal of Formal Logic Paul-André Melliès POPL Princeton University Proof theory Rocq Saarland University Simon Boulier Théo Winterhalter types type theory University of Amsterdam University of Birmingham University of Cambridge University of Oxford Valeria de Paiva