Observable Properties of Higher Order Functions that Dynamically Create Local Names, or What's new? - Andrew M. Pitts; Ian David Bede Stark (MFCS, 1993)

Names and higher-order functions. - Ian David Bede Stark (1994)

A Fully Abstract Domain Model for the pi-Calculus. - Ian Stark (LICS, 1996)

Categorical Models for Local Names. - Ian Stark (LISP Symb. Comput., 1996)

Presheaf Models for the pi-Calculus. - Gian Luca Cattani; Ian Stark; Glynn Winskel (Category Theory and Computer Science, 1997)

Names, Equations, Relations: Practical Ways to Reason about new. - Ian Stark (TLCA, 1997)

Names, Equations, Relations: Practical Ways to Reason About New. - Ian Stark (Fundam. Informaticae, 1998)

A Distributed Pi-Calculus with Local Areas of Communication. - Tom Chothia; Ian Stark (HLCL, 2000)

Automatic Verification of Java Design Patterns. - Alex Blewitt; Alan Bundy; Ian Stark (ASE, 2001)

Encoding Distributed Areas and Local Communication into the pi-Calculus. - Tom Chothia; Ian Stark (EXPRESS, 2001)

Grail: a functional form for imperative mobile code. - Lennart Beringer; Kenneth MacKenzie; Ian Stark (FGC, 2003)

Mobile Resource Guarantees for Smart Devices. - David Aspinall 001; Stephen Gilmore; Martin Hofmann 001; Donald Sannella; Ian Stark (CASSIS, 2004)

A Dependent Type Theory with Names and Binding. - Ulrich Schöpp; Ian Stark (CSL, 2004)

Nominal Games and Full Abstraction for the Nu-Calculus. - Samson Abramsky; Dan R. Ghica; Andrzej S. Murawski; C.-H. Luke Ong; Ian David Bede Stark (LICS, 2004)

Free-Algebra Models for the pi-Calculus. - Ian Stark (FoSSaCS, 2005)

Automatic verification of design patterns in Java. - Alex Blewitt; Alan Bundy; Ian Stark (ASE, 2005)

Mobile Resource Guarantees (project evaluation paper). - Donald Sannella; Martin Hofmann 001; David Aspinall 001; Stephen Gilmore; Ian Stark; Lennart Beringer; Hans-Wolfgang Loidl; Kenneth MacKenzie; Alberto Momigliano; Olha Shkaravska (Trends in Functional Programming, 2005)

Reducibility and TT-Lifting for Computation Types. - Sam Lindley; Ian Stark (TLCA, 2005)

MOBIUS: Mobility, Ubiquity, Security. - Gilles Barthe; Lennart Beringer; Pierre Crégut; Benjamin Grégoire; Martin Hofmann 001; Peter Müller 001; Erik Poll; Germán Puebla; Ian Stark; Eric Vétillard (TGC, 2006)

Safety Guarantees from Explicit Resource Management. - David Aspinall 001; Patrick Maier 001; Ian Stark (FMCO, 2007)

Monitoring External Resources in Java MIDP. - David Aspinall 001; Patrick Maier 001; Ian Stark (REM@ESORICS, 2007)

The Continuous pi-Calculus: A Process Algebra for Biochemical Modelling. - Marek Kwiatkowski; Ian Stark (CMSB, 2008)

Free-algebra models for the pi -calculus. - Ian Stark (Theor. Comput. Sci., 2008)

Certified Complexity. - R. Armadio; Andrea Asperti; Nicholas Ayache; Brian Campbell 001; Dominic P. Mulligan; Randy Pollack; Yann Régis-Gianas; Claudio Sacerdoti Coen; Ian Stark (FET, 2011)

Stochastic Modelling of the Kai-based Circadian Clock. - Chris J. Banks; Allan Clark; Anastasis Georgoulas; Stephen Gilmore; Jane Hillston; Dimitrios Milios; Ian Stark (PASM/PDMC, 2012)

Certified Complexity (CerCo). - Roberto M. Amadio; Nicholas Ayache; François Bobot; Jaap Boender; Brian Campbell 001; Ilias Garnier; Antoine Madet; James McKinna; Dominic P. Mulligan; Mauro Piccolo; Randy Pollack; Yann Régis-Gianas; et al. (FOPARA, 2013)

A logic of behaviour in context. - Chris J. Banks; Ian Stark (Inf. Comput., 2014)

Analysis of a Post-translational Oscillator Using Process Algebra and Spatio-Temporal Logic. - Chris J. Banks; Daniel D. Seaton; Ian Stark (CMSB, 2015)

Extracting behaviour from an executable instruction set model. - Brian Campbell 001; Ian Stark (FMCAD, 2016)

Randomised testing of a microprocessor model using SMT-solver state generation. - Brian Campbell 001; Ian Stark (Sci. Comput. Program., 2016)

A More Sensitive Context. - Chris J. Banks; Ian Stark (CoRR, 2017)

Triangulating context lemmas. - Craig McLaughlin; James McKinna; Ian Stark (CPP, 2018)

The Bond-Calculus: A Process Algebra for Complex Biological Interaction Dynamics. - Thomas Wright; Ian Stark (CoRR, 2018)

Foreword. - Martin Hofmann 001; David Aspinall 001; Brian Campbell 001; Ian Stark; Perdita Stevens (Theor. Comput. Sci., 2018)

ISA semantics for ARMv8-a, RISC-v, and CHERI-MIPS. - Alasdair Armstrong; Thomas Bauereiss; Brian Campbell 001; Alastair Reid 001; Kathryn E. Gray; Robert M. Norton; Prashanth Mundkur; Mark Wassell; Jon French; Christopher Pulte; Shaked Flur; Ian Stark; et al. (Proc. ACM Program. Lang., 2019)

Property-Directed Verified Monitoring of Signal Temporal Logic. - Thomas Wright; Ian Stark (RV, 2020)

Modelling Patterns of Gene Regulation in the bond-calculus. - Thomas Wright; Ian Stark (SASB, 2020)

Rigorous engineering for hardware security: Formal modelling and proof in the CHERI design and implementation process. - Kyndylan Nienhuis; Alexandre Joannou; Thomas Bauereiss; Anthony C. J. Fox; Michael Roe; Brian Campbell 001; Matthew Naylor; Robert M. Norton; Simon W. Moore; Peter G. Neumann; Ian Stark; Robert N. M. Watson; et al. (SP, 2020)

Technical Report: Property-Directed Verified Monitoring of Signal Temporal Logic. - Thomas Wright; Ian Stark (CoRR, 2020)

Fast and Correct Load-Link/Store-Conditional Instruction Handling in DBT Systems. - Martin Kristien; Tom Spink; Brian Campbell 001; Susmit Sarkar; Ian Stark; Björn Franke; Igor Böhm; Nigel P. Topham (IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 2020)

Neuro-Positionality in User-Centered Design: : The Case of Student Disability Services. - Ian Stark (SIGDOC, 2021)

Verified Security for the Morello Capability-enhanced Prototype Arm Architecture. - Thomas Bauereiss; Brian Campbell 001; Thomas Sewell; Alasdair Armstrong; Lawrence Esswood; Ian Stark; Graeme Barnes; Robert N. M. Watson; Peter Sewell (ESOP, 2022)

Formal Mechanised Semantics of CHERI C: Capabilities, Undefined Behaviour, and Provenance. - Vadim Zaliva; Kayvan Memarian; Ricardo Almeida 003; Jessica Clarke 001; Brooks Davis; Alexander Richardson 001; David Chisnall; Brian Campbell 001; Ian Stark; Robert N. M. Watson; Peter Sewell (ASPLOS (1), 2024)

Static Analysis for Transitioning to CHERI C/C++. - Irina Dudina; Ian Stark (SOAP@PLDI, 2024)

A CHERI C Memory Model for Verified Temporal Safety. - Vadim Zaliva; Kayvan Memarian; Brian Campbell 001; Ricardo Almeida 003; Nathaniel Wesley Filardo; Ian Stark; Peter Sewell (CPP, 2025)

Morello-Cerise: A Proof of Strong Encapsulation for the Arm Morello Capability Hardware Architecture. - Angus Hammond; Ricardo Almeida 003; Thomas Bauereiss; Brian Campbell 001; Ian Stark; Peter Sewell (Proc. ACM Program. Lang., 2025)

Static analysis to make the most of CHERI C/C++ for existing code: improving memory safety at scale. - Irina Dudina; Ian Stark (Int. J. Softw. Tools Technol. Transf., 2025)