Publications

Infinite horizon extensive form games, coalgebraically

Capucci Matteo, Ghani Neil, Kupke Clemens, Ledent Jérémy, Nordvall Forsberg Fredrik

Mathematics for Computation (2023) (2023)

https://doi.org/10.1142/9789811245220_0008

Translating extensive form games to open games with agency

Capucci Matteo, Ghani Neil, Ledent Jérémy, Nordvall Forsberg Fredrik

Applied Category Theory 2021 (2021)

Compositional Game Theory, compositionally

Atkey Robert, Gavranović Bruno, Ghani Neil, Kupke Clemens, Ledent Jérémy, Nordvall Forsberg Fredrik

Applied Category Theory 2020 (2020)

Three equivalent ordinal notation systems in cubical Agda

Nordvall Forsberg Fredrik, Xu Chuangjie, Ghani Neil

CPP 2020 : Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs , pp. 172–185 (2020)

https://doi.org/10.1145/3372885.3373835

Compositional game theory with mixed strategies : probabilistic open games using a distributive law

Ghani Neil, Kupke Clemens, Lambert Alasdair, Nordvall Forsberg Fredrik

Applied category theory conference 2019, pp. 1-12 (2019)

Universal properties for universal types in bifibrational parametricity

Ghani Neil, Nordvall Forsberg Fredrik, Orsanigo Federico

Mathematical Structures in Computer Science Vol 29, pp. 810–827 (2019)

https://doi.org/10.1017/S0960129518000336

More publications

Professional Activities

Connected Places Exploration Workshop

Participant

26/9/2019

Contributed talk TYPES 2017: "Variations on inductive-recursive defnitions closed under composition"

Contributor

31/5/2017

Contributed talk TYPES 2016: "A Type Theory for Comprehensive Parametric Polymorphism"

Contributor

23/5/2016

Contributed talk TYPES 2015: "Two-dimensional proof-relevant parametricity"

Contributor

21/5/2015

More professional activities

Projects

Sea lice dispersal models

Waites, William (Principal Investigator) Ghani, Neil (Co-investigator) Mardare, Radu (Co-investigator) Revie, Crawford (Co-investigator)

08-Jan-2024 - 31-Jan-2024

Trusted Systems

Ghani, Neil (Principal Investigator) McBride, Conor (Co-investigator) Nordvall Forsberg, Fredrik (Co-investigator)

01-Jan-2019 - 30-Jan-2024

Trusted Systems

Ghani, Neil (Co-investigator) McBride, Conor (Principal Investigator) Nordvall Forsberg, Fredrik (Co-investigator)

01-Jan-2019 - 30-Jan-2023

Doctoral Training Partnership 2018-19 University of Strathclyde | Gavranovic, Bruno

Ghani, Neil (Principal Investigator) Weir, George (Co-investigator) Gavranovic, Bruno (Research Co-investigator)

01-Jan-2019 - 07-Jan-2024

Homotopy Type Theory: Programming and Verification

Ghani, Neil (Principal Investigator) McBride, Conor (Co-investigator)

"The cost of software failure is truly staggering. Well known
individual cases include the Mars Climate Orbiter failure
(£80 million), Ariane Rocket disaster (£350 million), Pentium
Chip Division failure (£300 million), and more recently the heartbleed
bug (est. £400 million). There are many, many more examples. Even worse,
failures such as one in the Patriot Missile System and another
in the Therac-25 radiation system have cost lives. More generally, a
2008 study by the US government estimated that faulty
software costs the US economy £100 billion
annually.

There are many successful approaches to software verification
(testing, model checking etc). One approach is to find mathematical
proofs that guarantees of software correctness. However, the
complexity of modern software means that hand-written mathematical
proofs can be untrustworthy and this has led to a growing desire for
computer-checked proofs of software correctness.
Programming languages and interactive proof systems like Coq, Agda,
NuPRL and Idris have been developed based on a formal system called
Martin Type Theory. In these systems, we can not only write
programs, but we can also express properties of programs using types,
and write programs to express proofs that our programs are correct.
In this way, both large mathematical theorems such as the Four Colour
Theorem, and large software systems such as the CompCert C compiler
have been formally verified. However, in such large projects, the
issue of scalability arises: how can we use these systems to build large
libraries of verified software in an effective way?

This is related to the problem of reusability and modularity: a
component in a software system should be replaceable by another which
behaves the same way even though it may be constructed in a completely
different way. That is, we need an extensional equality which is
computationally well behaved (that is, we want to run programs using
this equality). Finding such an ty is a fundamental and
difficult problem which has remained unresolved for over 40 years.

But now it looks like we might have a solution! Fields medallist
Vladimir Voevodsky has come up with a completely different take on the
problem by thinking of equalities as paths such as those which occur
in one of the most abstract branches of mathematics, namely homotopy
theory, leading to Homotopy Type Theory (HoTT). In HoTT, two objects
are completely interchangeable if they behave the same way. However,
most presentations of HoTT involve axioms which lack computational
justification and, as a result, we do not have programming languages
or verification systems based upon HoTT. The goal of our project is
to fix that, thereby develop the first of a new breed of HoTT-based
programming languages and verification systems, and develop case
studies which demonstrate the power of HoTT to programmers and
those interested in formal verification.

We are an ideal team to undertake this research because i) we have
unique skills and ideas ranging from the foundations of HoTT to the
implementation and deployment of programming language and verification
tools; and ii) the active collaboration of the most important figures
in the area (including Voevodsky) as well as industrial participation
to ensure that we keep in mind our ultimate goal -- usable programming
language and verification tools."

01-Jan-2015 - 30-Jan-2019

Doctoral Training Partnership (DTA - University of Strathclyde) | Dunne, Kevin

Duncan, Ross (Principal Investigator) Ghani, Neil (Co-investigator) Dunne, Kevin (Research Co-investigator)

01-Jan-2014 - 19-Jan-2019

More projects