Epigram reloaded: a standalone typechecker for ETT. - James Chapman 001; Thorsten Altenkirch; Conor McBride (Trends in Functional Programming, 2005)

Tait in One Big Step. - Thorsten Altenkirch; James Chapman 001 (MSFP@MPC, 2006)

Type Theory Should Eat Itself. - James Chapman 001 (LFMTP@LICS, 2008)

Big-step normalisation. - Thorsten Altenkirch; James Chapman 001 (J. Funct. Program., 2009)

Type checking and normalisation. - James Chapman 001 (2009)

The gentle art of levitation. - James Chapman 001; Pierre-Évariste Dagand; Conor McBride; Peter Morris (ICFP, 2010)

Normalization by Evaluation in the Delay Monad: A Case Study for Coinduction via Copatterns and Sized Types. - Andreas Abel 001; James Chapman 001 (MSFP, 2014)

When is a container a comonad? - Danel Ahman; James Chapman 001; Tarmo Uustalu (Log. Methods Comput. Sci., 2014)

Relative Monads Formalised. - Thorsten Altenkirch; James Chapman 001; Tarmo Uustalu (J. Formaliz. Reason., 2014)

Monads need not be endofunctors. - Thorsten Altenkirch; James Chapman 001; Tarmo Uustalu (Log. Methods Comput. Sci., 2015)

Type-and-scope safe programs and their proofs. - Guillaume Allais; James Chapman 001; Conor McBride; James McKinna (CPP, 2017)

Formalizing Restriction Categories. - James Chapman 001; Tarmo Uustalu; Niccolò Veltri (J. Formaliz. Reason., 2017)

A type and scope safe universe of syntaxes with binding: their semantics and proofs. - Guillaume Allais; Robert Atkey; James Chapman 001; Conor McBride; James McKinna (Proc. ACM Program. Lang., 2018)

System F in Agda, for Fun and Profit. - James Chapman 001; Roman Kireev; Chad Nester; Philip Wadler (MPC, 2019)

Quotienting the delay monad by weak bisimilarity. - James Chapman 001; Tarmo Uustalu; Niccolò Veltri (Math. Struct. Comput. Sci., 2019)

The Extended UTXO Model. - Manuel M. T. Chakravarty; James Chapman 001; Kenneth MacKenzie; Orestis Melkonian; Michael Peyton Jones; Philip Wadler (Financial Cryptography Workshops, 2020)

Native Custom Tokens in the Extended UTXO Model. - Manuel M. T. Chakravarty; James Chapman 001; Kenneth MacKenzie; Orestis Melkonian; Jann Müller; Michael Peyton Jones; Polina Vinogradova; Philip Wadler (ISoLA (3), 2020)

UTXOsf ma: UTXO with Multi-asset Support. - Manuel M. T. Chakravarty; James Chapman 001; Kenneth MacKenzie; Orestis Melkonian; Jann Müller; Michael Peyton Jones; Polina Vinogradova; Philip Wadler; Joachim Zahnentferner (ISoLA (3), 2020)

Flexible Formality Practical Experience with Agile Formal Methods. - Philipp Kant; Kevin Hammond; Duncan Coutts; James Chapman 001; Nicholas Clarke; Jared Corduan; Neil J. Davies; Javier Díaz; Matthias Güdemann; Wolfgang Jeltsch; Marcin Szamotulski; Polina Vinogradova (TFP, 2020)

Reasonable Agda is correct Haskell: writing verified Haskell using agda2hs. - Jesper Cockx; Orestis Melkonian; Lucas Escot; James Chapman 001; Ulf Norell (Haskell, 2022)

Mind Your Outcomes: The ΔQSD Paradigm for Quality-Centric Systems Development and Its Application to a Blockchain Case Study. - Seyed H. Haeri; Peter Thompson 002; Neil J. Davies; Peter Van Roy; Kevin Hammond; James Chapman 001 (Comput., 2022)

Algebraic Reasoning About Timeliness. - Seyed Hossein Haeri; Peter W. Thompson 002; Peter Van Roy; Magne Haveraaen; Neil J. Davies; Mikhail Barash; Kevin Hammond; James Chapman 001 (ICE, 2023)

Formal Specification of the Cardano Blockchain Ledger, Mechanized in Agda. - Andre Knispel; Orestis Melkonian; James Chapman 001; Alasdair Hill; Joosep Jääger; William J. DeMeo; Ulf Norell (FMBC@CAV, 2024)

Structured Contracts in the EUTxO Ledger Model. - Polina Vinogradova; Orestis Melkonian; Philip Wadler; Manuel M. T. Chakravarty; Jacco Krijnen; Michael Peyton Jones; James Chapman 001; Tudor Ferariu (FMBC@CAV, 2024)

Applying Continuous Formal Methods to Cardano (Experience Report). - James Chapman 001; Arnaud Bailly; Polina Vinogradova (FUNARCH, 2024)

IntersectMBO/formal-ledger-specifications. - Andre Knispel; Orestis Melkonian; James Chapman 001; Alasdair Hill; Joosep Jääger; William J. DeMeo; Ulf Norell (DROPS Artifacts, 2024)

A Readable and Computable Formalization of the Streamlet Consensus Protocol. - Mauro Jaskelioff; Orestis Melkonian; James Chapman 001 (FMBC, 2025)

Program Logics for Ledgers. - Orestis Melkonian; Wouter Swierstra; James Chapman 001 (FMBC, 2025)