329 citations · 459 across the 19 of their papers we have counts for
18 papers · 1 filter
DRAFT: A Formally Verified Constructive Proof of the Consistency of Peano Arithmetic Using Ordinal Assignments
Aaron Bryce, Rajeev Gore'
Gentzen's 1936 proof of the consistency of Peano Arithmetic was a significant result in the foundations of mathematics. We provide here a modified version of the proof, based on Gö…
A new calculus for intuitionistic Strong Löb logic: strong termination and cut-elimination, formalised
Ian Shillito, Iris van der Giessen, Rajeev Goré +1
We provide a new sequent calculus that enjoys syntactic cut-elimination and strongly terminating backward proof search for the intuitionistic Strong Löb logic , an intuit…
Syntactic Interpolation for Tense Logics and Bi-Intuitionistic Logic via Nested Sequents
Tim Lyon, Alwen Tiu, Rajeev Goré +1
We provide a direct method for proving Craig interpolation for a range of modal and intuitionistic logics, including those containing a "converse" modality. We demonstrate this met…
Syntactic cut-elimination and backward proof-search for tense logic via linear nested sequents (Extended version)
Rajeev Goré, Björn Lellmann
We give a linear nested sequent calculus for the basic normal tense logic Kt. We show that the calculus enables backwards proof-search, counter-model construction and syntactic cut…
A case study in formal verification of a Java program
Dmitry Brizhinev, Rajeev Goré
We describe a successful attempt to formally verify a simple genetic algorithm written in Java. To this end, we compare several formal verification tools designed for Java, and sel…
Modular Labelled Sequent Calculi for Abstract Separation Logics
Zhé Hóu, Ranald Clouston, Rajeev Goré +1
Abstract separation logics are a family of extensions of Hoare logic for reasoning about programs that manipulate resources such as memory locations. These logics are "abstract" be…