329 citations · 374 across the 11 of their papers we have counts for
15 papers
Embedding Modal Logics into Logics of Bunched Implications
Daniele Sansoni, Ranald Clouston
We present a new proof of the embedding of the classical modal logic S4 into the logic of Boolean Bunched Implications (BBI). While the original proof is semantical, this proof is…
Duality for Constructive Modal Logics: from Sahqlvist to Goldblatt-Thomason
Jim de Groot, Ian Shillito, Ranald Clouston
We carry out a semantic study of the constructive modal logic CK. We provide a categorical duality linking the algebraic and birelational semantics of the logic. We then use this t…
Semantical Analysis of Intuitionistic Modal Logics between CK and IK
Jim de Groot, Ian Shillito, Ranald Clouston
The intuitionistic modal logics considered between Constructive K (CK) and Intuitionistic K (IK) differ in their treatment of the possibility (diamond) connective. It was recently…
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…
Modal Dependent Type Theory and Dependent Right Adjoints
Lars Birkedal, Ranald Clouston, Bassel Mannaa +3
In recent years we have seen several new models of dependent type theory extended with some form of modal necessity operator, including nominal type theory, guarded and clocked typ…
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…
Fitch-Style Modal Lambda Calculi
Ranald Clouston
Fitch-style modal deduction, in which modalities are eliminated by opening a subordinate proof, and introduced by shutting one, were investigated in the 1990s as a basis for lambda…
Guarded Cubical Type Theory
Lars Birkedal, Aleš Bizjak, Ranald Clouston +3
This paper improves the treatment of equality in guarded dependent type theory (GDTT), by combining it with cubical type theory (CTT). GDTT is an extensional type theory with guard…
Guarded Cubical Type Theory: Path Equality for Guarded Recursion
Lars Birkedal, Aleš Bizjak, Ranald Clouston +3
This paper improves the treatment of equality in guarded dependent type theory (GDTT), by combining it with cubical type theory (CTT). GDTT is an extensional type theory with guard…
Guarded Dependent Type Theory with Coinductive Types
Aleš Bizjak, Hans Bugge Grathwohl, Ranald Clouston +2
We present guarded dependent type theory, gDTT, an extensional dependent type theory with a `later' modality and clock quantifiers for programming and proving with guarded recursiv…
Programming and Reasoning with Guarded Recursion for Coinductive Types
Ranald Clouston, Aleš Bizjak, Hans Bugge Grathwohl +1
We present the guarded lambda-calculus, an extension of the simply typed lambda-calculus with guarded recursive and coinductive types. The use of guarded recursive types ensures th…
Status of the Higgs Singlet Extension of the Standard Model after LHC Run 1
Tania Robens, Tim Stefaniak
We discuss the current status of theoretical and experimental constraints on the real Higgs singlet extension of the Standard Model. For the second neutral (non-standard) Higgs bos…
Annotation-Free Sequent Calculi for Full Intuitionistic Linear Logic -- Extended Version
Ranald Clouston, Jeremy Dawson, Rajeev Gore +1
Full Intuitionistic Linear Logic (FILL) is multiplicative intuitionistic linear logic extended with par. Its proof theory has been notoriously difficult to get right, and existing…
Proof search for propositional abstract separation logics via labelled sequents
Zhe Hou, Ranald Clouston, Rajeev Gore +1
Separation logics are a family of extensions of Hoare logic for reasoning about programs that mutate memory. These logics are "abstract" because they are independent of any particu…
Nominal Logic with Equations Only
Ranald Clouston
Many formal systems, particularly in computer science, may be captured by equations modulated by side conditions asserting the "freshness of names"; these can be reasoned about wit…