James Chapman

36 papers A 1B 4C 2Journal 11Unranked 14
YearRankTypeTitle / Venue / Authors
2026 J jnl
Algebraic reasoning for timeliness-guided system design.
J. Log. Algebraic Methods Program.
Seyed Hossein Haeri, Peter Van Roy, Heinrich Apfelmus, Peter Thompson, Neil J. Davies, Magne Haveraaen, Mikhail Barash, Kevin Hammond, James Chapman, Artjoms Sinkarovs
2025 — conf
A Readable and Computable Formalization of the Streamlet Consensus Protocol.
FMBC
Mauro Jaskelioff, Orestis Melkonian, James Chapman
2025 — conf
Program Logics for Ledgers.
FMBC
Orestis Melkonian, Wouter Swierstra, James Chapman
2024 — conf
Applying Continuous Formal Methods to Cardano (Experience Report).
FUNARCH
James Chapman, Arnaud Bailly, Polina Vinogradova
2024 — conf
Formal Specification of the Cardano Blockchain Ledger, Mechanized in Agda.
FMBC@CAV
Andre Knispel, Orestis Melkonian, James Chapman, Alasdair Hill, Joosep Jääger, William J. DeMeo, Ulf Norell
2024 — conf
Structured Contracts in the EUTxO Ledger Model.
FMBC@CAV
Polina Vinogradova, Orestis Melkonian, Philip Wadler, Manuel M. T. Chakravarty, Jacco Krijnen, Michael Peyton Jones, James Chapman, Tudor Ferariu
2023 — conf
Algebraic Reasoning About Timeliness.
ICE
Seyed Hossein Haeri, Peter W. Thompson, Peter Van Roy, Magne Haveraaen, Neil J. Davies, Mikhail Barash, Kevin Hammond, James Chapman
2022 J jnl
Mind Your Outcomes: The ΔQSD Paradigm for Quality-Centric Systems Development and Its Application to a Blockchain Case Study.
Comput.
Seyed H. Haeri, Peter Thompson, Neil J. Davies, Peter Van Roy, Kevin Hammond, James Chapman
2022 C conf
Reasonable Agda is correct Haskell: writing verified Haskell using agda2hs.
Haskell
Jesper Cockx, Orestis Melkonian, Lucas Escot, James Chapman, Ulf Norell
2021 J jnl
A type- and scope-safe universe of syntaxes with binding: their semantics and proofs.
J. Funct. Program.
Guillaume Allais, Robert Atkey, James Chapman, Conor McBride, James McKinna
2020 J jnl
A Type and Scope Safe Universe of Syntaxes with Binding: Their Semantics and Proofs.
CoRR
Guillaume Allais, Robert Atkey, James Chapman, Conor McBride, James McKinna
2020 — conf
Flexible Formality Practical Experience with Agile Formal Methods.
TFP
Philipp Kant, Kevin Hammond, Duncan Coutts, James Chapman, Nicholas Clarke, Jared Corduan, Neil J. Davies, Javier Díaz, Matthias Güdemann, Wolfgang Jeltsch, Marcin Szamotulski, Polina Vinogradova
2020 — conf
Native Custom Tokens in the Extended UTXO Model.
ISoLA (3)
Manuel M. T. Chakravarty, James Chapman, Kenneth MacKenzie, Orestis Melkonian, Jann Müller, Michael Peyton Jones, Polina Vinogradova, Philip Wadler
2020 — conf
The Extended UTXO Model.
Financial Cryptography Workshops
Manuel M. T. Chakravarty, James Chapman, Kenneth MacKenzie, Orestis Melkonian, Michael Peyton Jones, Philip Wadler
2020 — conf
UTXO
ISoLA (3)
Manuel M. T. Chakravarty, James Chapman, Kenneth MacKenzie, Orestis Melkonian, Jann Müller, Michael Peyton Jones, Polina Vinogradova, Philip Wadler, Joachim Zahnentferner
2019 J jnl
Quotienting the delay monad by weak bisimilarity.
Math. Struct. Comput. Sci.
James Chapman, Tarmo Uustalu, Niccolò Veltri
2019 B conf
System F in Agda, for Fun and Profit.
MPC
James Chapman, Roman Kireev, Chad Nester, Philip Wadler
2018 J jnl
A type and scope safe universe of syntaxes with binding: their semantics and proofs.
Proc. ACM Program. Lang.
Guillaume Allais, Robert Atkey, James Chapman, Conor McBride, James McKinna
2017 J jnl
Formalizing Restriction Categories.
J. Formaliz. Reason.
James Chapman, Tarmo Uustalu, Niccolò Veltri
2017 B conf
Type-and-scope safe programs and their proofs.
CPP
Guillaume Allais, James Chapman, Conor McBride, James McKinna
2016 — ed.
Proceedings of the 1st International Workshop on Type-Driven Development, TyDe@ICFP 2016, Nara, Japan, September 18, 2016
TyDe@ICFP
James Chapman, Wouter Swierstra
2015 J jnl
Monads need not be endofunctors.
Log. Methods Comput. Sci.
Thorsten Altenkirch, James Chapman, Tarmo Uustalu
2015 C conf
Quotienting the Delay Monad by Weak Bisimilarity.
ICTAC
James Chapman, Tarmo Uustalu, Niccolò Veltri
2014 — conf
Normalization by Evaluation in the Delay Monad: A Case Study for Coinduction via Copatterns and Sized Types.
MSFP
Andreas Abel, James Chapman
2014 J jnl
Relative Monads Formalised.
J. Formaliz. Reason.
Thorsten Altenkirch, James Chapman, Tarmo Uustalu
2014 J jnl
When is a container a comonad?
Log. Methods Comput. Sci.
Danel Ahman, James Chapman, Tarmo Uustalu
2012 — ed.
Proceedings Fourth Workshop on Mathematically Structured Functional Programming, MSFP@ETAPS 2012, Tallinn, Estonia, 25 March 2012.
MSFP@ETAPS
James Chapman, Paul Blain Levy
2012 B conf
When Is a Container a Comonad?
FoSSaCS
Danel Ahman, James Chapman, Tarmo Uustalu
2010 B conf
Monads Need Not Be Endofunctors.
FoSSaCS
Thorsten Altenkirch, James Chapman, Tarmo Uustalu
2010 — ed.
Proceedings of the 3rd ACM SIGPLAN Workshop on Mathematically Structured Functional Programming, MSFP@ICFP 2010, Baltimore, MD, USA, September 25, 2010.
MSFP@ICFP
Venanzio Capretta, James Chapman
2010 A conf
The gentle art of levitation.
ICFP
James Chapman, Pierre-Évariste Dagand, Conor McBride, Peter Morris
2009 J jnl
Big-step normalisation.
J. Funct. Program.
Thorsten Altenkirch, James Chapman
2009 — —
Type checking and normalisation.
James Chapman
2008 — conf
Type Theory Should Eat Itself.
LFMTP@LICS
James Chapman
2006 — conf
Tait in One Big Step.
MSFP@MPC
Thorsten Altenkirch, James Chapman
2005 — conf
Epigram reloaded: a standalone typechecker for ETT.
Trends in Functional Programming
James Chapman, Thorsten Altenkirch, Conor McBride