The following pages link to James Brotherston (Q1401935):
Displayed 26 items.
- A formalised first-order confluence proof for the \(\lambda\)-calculus using one-sorted variable names. (Q1401936) (← links)
- Realizability in cyclic proof: extracting ordering information for infinite descent (Q1694474) (← links)
- Bunched logics displayed (Q1935559) (← links)
- Reasoning over permissions regions in concurrent separation logic (Q2226736) (← links)
- Biabduction (and related problems) in array separation logic (Q2405270) (← links)
- (Q2778886) (← links)
- Machine-Checked Interpolation Theorems for Substructural Logics Using Display Calculi (Q2817943) (← links)
- Model checking for symbolic-heap separation logic with inductive predicates (Q2828247) (← links)
- The Mechanisation of Barendregt-Style Equational Proofs (the Residual Perspective) (Q2841232) (← links)
- Craig Interpolation in Displayable Logics (Q3010362) (← links)
- Sequent calculi for induction and infinite descent (Q3103982) (← links)
- A Unified Display Proof Theory for Bunched Logic (Q3178253) (← links)
- Undecidability of Propositional Separation Logic and Its Neighbours (Q3189649) (← links)
- Cyclic proofs of program termination in separation logic (Q3189830) (← links)
- Disproving Inductive Entailments in Separation Logic via Base Pair Approximation (Q3455777) (← links)
- Classical BI: Its Semantics and Proof Theory (Q3575307) (← links)
- Formalised Inductive Reasoning in the Logic of Bunched Implications (Q3611996) (← links)
- A decision procedure for satisfiability in separation logic with inductive predicates (Q4635608) (← links)
- Automated Cyclic Entailment Proofs in Separation Logic (Q5200020) (← links)
- Classical BI (Q5261530) (← links)
- Sub-classical Boolean Bunched Logics and the Meaning of Par (Q5351966) (← links)
- Parametric completeness for separation theories (Q5408441) (← links)
- Automated Reasoning with Analytic Tableaux and Related Methods (Q5479270) (← links)
- Automatically verifying temporal properties of pointer programs with cyclic proof (Q5919481) (← links)
- Automatically verifying temporal properties of pointer programs with cyclic proof (Q5920091) (← links)
- On the complexity of pointer arithmetic in separation logic (Q6166154) (← links)