James Brotherston
James Brotherston
Reader in Logic and Computation at University College London
E-mail confirmado em ucl.ac.uk - Página inicial
Título
Citado por
Citado por
Ano
Sequent calculi for induction and infinite descent
J Brotherston, A Simpson
Journal of Logic and Computation 21 (6), 1177-1216, 2011
1032011
Cyclic proofs for first-order logic with inductive definitions
J Brotherston
International Conference on Automated Reasoning with Analytic Tableaux and …, 2005
1032005
A generic cyclic theorem prover
J Brotherston, N Gorogiannis, RL Petersen
Asian Symposium on Programming Languages and Systems, 350-367, 2012
922012
Cyclic proofs of program termination in separation logic
J Brotherston, R Bornat, C Calcagno
ACM SIGPLAN Notices 43 (1), 101-112, 2008
892008
Undecidability of propositional separation logic and its neighbours
J Brotherston, M Kanovich
2010 25th Annual IEEE Symposium on Logic in Computer Science, 130-139, 2010
702010
A decision procedure for satisfiability in separation logic with inductive predicates
J Brotherston, C Fuhs, JAN Pérez, N Gorogiannis
Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference …, 2014
662014
Automated cyclic entailment proofs in separation logic
J Brotherston, D Distefano, RL Petersen
International Conference on Automated Deduction, 131-146, 2011
632011
Sequent calculus proof systems for inductive definitions
J Brotherston
University of Edinburgh. College of Science and Engineering. School of …, 2006
562006
Complete sequent calculi for induction and infinite descent
J Brotherston, A Simpson
22nd Annual IEEE Symposium on Logic in Computer Science (LICS 2007), 51-62, 2007
532007
Parametric completeness for separation theories
J Brotherston, J Villard
ACM SIGPLAN Notices 49 (1), 453-464, 2014
482014
Formalised inductive reasoning in the logic of bunched implications
J Brotherston
International Static Analysis Symposium, 87-103, 2007
422007
Bunched logics displayed
J Brotherston
Studia Logica 100 (6), 1223-1254, 2012
372012
Cyclic abduction of inductively defined safety and termination preconditions
J Brotherston, N Gorogiannis
International Static Analysis Symposium, 68-84, 2014
362014
Model checking for symbolic-heap separation logic with inductive predicates
J Brotherston, N Gorogiannis, M Kanovich, R Rowe
ACM SIGPLAN Notices 51 (1), 84-96, 2016
272016
Automatic cyclic termination proofs for recursive procedures in separation logic
RNS Rowe, J Brotherston
Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and …, 2017
262017
Undecidability of propositional separation logic and its neighbours
J Brotherston, M Kanovich
Journal of the ACM (JACM) 61 (2), 1-43, 2014
262014
Classical BI: Its semantics and proof theory
J Brotherston, C Calcagno
arXiv preprint arXiv:1005.2340, 2010
262010
A formalised first-order confluence proof for the λ-calculus using one-sorted variable names
R Vestergaard, J Brotherston
Information and Computation 183 (2), 212-244, 2003
222003
A Formalised First-Order Confluence Proof for the λ-Calculus Using One-Sorted Variable Names (Barendregt Was Right after all... almost)
R Vestergaard, J Brotherston
International Conference on Rewriting Techniques and Applications, 306-321, 2001
222001
Classical BI: a logic for reasoning about dualising resources
J Brotherston, C Calcagno
ACM SIGPLAN Notices 44 (1), 328-339, 2009
212009
O sistema não pode executar a operação agora. Tente novamente mais tarde.
Artigos 1–20