-
Article
Open AccessDouble Negation Semantics for Generalisations of Heyting Algebras
This paper presents an algebraic framework for investigating proposed translations of classical logic into intuitionistic logic, such as the four negative translations introduced by Kolmogorov, Gödel, Gentzen ...
-
Chapter
Studying Algebraic Structures Using Prover9 and Mace4
In this chapter we present a case study, drawn from our research work, on the application of a fully automated theorem prover together with an automatic counter-example generator in the investigation of a clas...
-
Chapter and Conference Paper
Selection Equilibria of Higher-Order Games
In applied game theory the modelling of each player’s intentions and motivations is a key aspect. In classical game theory these are encoded in the payoff functions. In previous work [2, 4] a novel way of modelli...
-
Chapter and Conference Paper
Higher-Order Decision Theory
This paper investigates a surprising relationship between decision theory and proof theory. Using constructions originating in proof theory based on higher-order functions, so called quantifiers and selection fun...
-
Chapter
A Game-Theoretic Computational Interpretation of Proofs in Classical Analysis
It has been shown by Escardó and the first author that a functional interpretation of proofs in analysis can be given by the product of selection functions, a mode of recursion that has an intuitive reading in...
-
Article
A Hoare logic for linear systems
We consider reasoning about linear systems expressed as block diagrams that give a graphical representation of a system of differential equations or recurrence equations. We use the notion of additive relation...
-
Chapter
(Dual) Hoops Have Unique Halving
Continuous logic extends the multi-valued Łukasiewicz logic by adding a halving operator on propositions. This extension is designed to give a more satisfactory model theory for continuous structures. The sema...
-
Chapter and Conference Paper
The Peirce Translation and the Double Negation Shift
We develop applications of selection functions to proof theory and computational extraction of witnesses from proofs in classical analysis. The main novelty is a translation of classical minimal logic into min...
-
Chapter and Conference Paper
Computational Interpretations of Analysis via Products of Selection Functions
We show that the computational interpretation of full comprehension via two well-known functional interpretations (dialectica and modified realizability) corresponds to two closely related infinite products of...
-
Chapter and Conference Paper
Functional Interpretations of Intuitionistic Linear Logic
We present three functional interpretations of intuitionistic linear logic and show how these correspond to well-known functional interpretations of intuitionistic logic via embeddings of IL ...
-
Chapter and Conference Paper
Hybrid Functional Interpretations
We show how different functional interpretations can be combined via a multi-modal linear logic. A concrete hybrid of Kreisel’s modified realizability and Gödel’s Dialectica is presented, and several small app...
-
Chapter and Conference Paper
Computational Interpretations of Classical Linear Logic
We survey several computational interpretations of classical linear logic based on two-player one-move games. The moves of the games are higher-order functionals in the language of finite types. All interpreta...
-
Chapter and Conference Paper
Understanding and Using Spector’s Bar Recursive Interpretation of Classical Analysis
This note reexamines Spector’s remarkable computational interpretation of full classical analysis. Spector’s interpretation makes use of a rather abstruse recursion schema, so-called bar recursion, used to int...
-
Chapter and Conference Paper
Hoare Logic in the Abstract
We present an abstraction of Hoare logic to traced symmetric monoidal categories, a very general framework for the theory of systems. We first identify a particular class of functors – which we call ‘verificat...
-
Chapter and Conference Paper
Reporting exact and approximate regular expression matches
While much work has been done on determining if a document or a line of a document contains an exact or approximate match to a regular expression, less effort has been expended in formulating and determining w...
