Dr Conor McBride

Reader

Computer and Information Sciences

Publications

Type-and-scope safe programs and their proofs
Allais Guillaume, Chapman James, McBride Conor, McKinna James
CPP 2017, (2017)
http://dx.doi.org/10.1145/3018610.3018613
Do Be Do Be Do
Lindley Sam, McBride Conor, McLaughlin Craig
POPL'2017, pp. 500-514, (2017)
http://dx.doi.org/10.1145/3009837.3009897
I got plenty o’ nuttin’
McBride Conor
A List of Successes That Can Change the WorldLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) Vol 9600, pp. 207-233, (2016)
http://dx.doi.org/10.1007/978-3-319-30936-1_12
A List of Successes That Can Change the World : Essays Dedicated to Philip Wadler on the Occasion of His 60th Birthday
Lindley Sam, McBride Conor, Trinder Phil, Sannella Don
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) Vol 9600, (2016)
http://dx.doi.org/10.1007/978-3-319-30936-1
Turing-completeness totally free
McBride Conor
Mathematics of Program Construction, pp. 257-275, (2015)
http://dx.doi.org/10.1007/978-3-319-19797-5_13
How to keep your neighbours in order
McBride Conor
ICFP '14 Proceedings of the 19th ACM SIGPLAN International Conference on Functional Programming, pp. 297-309, (2014)
http://dx.doi.org/10.1145/2628136.2628163

more publications

Professional activities

Invited Lecture Courses on Dependently Typed Programming Oregon Programming Languages Summer School, USA, 2010
Invited speaker
2010
IFIP Working Group (External organisation)
Member
2010
ICFP 2009
Member of programme committee
2009
Journal of Functional Programming (Journal)
Editor
1/2008
Vol 19, Issues 3 & 4 (Special Issue on Mathematically Structured Functional Programming
Guest editor
1/2008

more professional activities

Projects

Doctoral Training Grant | Andjelkovic, Stevan
McBride, Conor (Principal Investigator) Ghani, Neil (Co-investigator) Andjelkovic, Stevan (Research Co-investigator)
Period 01-Oct-2011 - 01-Apr-2015
Real World Data with Dependent Types: Integrity and Interoperation
McBride, Conor (Principal Investigator)
Period 01-Apr-2016 - 31-Mar-2019
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."
Period 01-Apr-2015 - 31-Mar-2019
CORCON (FP7 IRSES)
Ghani, Neil (Principal Investigator) Kupke, Clemens (Co-investigator) McBride, Conor (Co-investigator)
Period 01-Jan-2014 - 31-Dec-2017
Haskell Types with Added Value
McBride, Conor (Principal Investigator)
"Good ideas, like lightning, take the most conductive path to earth. This one-year project takes advantage of fresh technological insights to narrow the spark-gap from theoretical research to the programming mainstream. In the last decade, dependent types --- capturing relative notions of data validity --- have jumped from logics and proof systems to programming. Prototype languages such as Cayenne, ATS, Agda and our own Epigram teach us how to characterize data precisely, but none has a coherent treatment of interaction in applications. This project will bring the basics of dependent types to application development now, not via a prototype, but with Haskell, a mature functional programming language with growing traction, thanks to the Glasgow Haskell Compiler (GHC), now developed under the Microsoft aegis. To make this jump, we must give practical answers to theoretical questions about the mathematical structures which underpin interactive and distributed systems. We must take the blackboard to the motherboard.

The tool which enables this project is our GHC preprocessor, the Strathclyde Haskell Enhancement (SHE), which mechanizes a partial translation from 'dependently typed Haskell' to Haskell as it stands. Up and running, SHE has already delivered the basics of our approach, leading to an article accepted in 2011 by the Journal of Functional Programming, and spurring deeper investigation of both the mathematics of dependently typed interaction and the engineering challenge of scaling up. Through theoretical research, library design and case study, we shall deliver progress across this spectrum through papers and open source software. GHC is adopting our functionality, but we do not need to wait. SHE can sustain low-cost exploration, putting an effective toolkit in users' hands now, as well as informing the future prospectuses both for dependent types in Haskell and for programming interaction in the next generation of functional languages. Haskellers recognize the need: Microsoft currently funds a PhD at Strathclyde on numerical dependency in Haskell types.

This project is, then, a double fix: it imports dependent types from tomorrow's languages to today's, and it allows us to guide tomorrow's dependently typed languages towards principled approaches to production software. We have proven track records in theoretical research and professional software development, key ideas to change programming for the better, and the skills to deliver world-leading research."
Period 01-Jul-2012 - 30-Jun-2013
Reusability and Dependent Types
Ghani, Neil (Principal Investigator) McBride, Conor (Co-investigator)
Robin Milner coined the slogan well typed programs cannot go wrong , advertising the strength of typed functional languages like MLand Haskell in using types to catch runtime errors. Nowadays, we can and want to go further: dependently typed programming exploits the power of very expressive type systems to deliver stronger guarantees but also additional support for software development, using types to guide the development process. This is witnessed by a recent surge of language proposals with the goal to harness the power of dependent types, e.g. Haskell with GADTs, Agda, Coq, Omega, Concoqtion, Guru, Ynot, Epigram and so on. However, expressive type systems have their price: more specific types frequently reduce the reusability of code, whose too-specific implementation type may not fit its current application. This phenomenon already shows up in the traditional Hindley-Milner style type system of ML and Haskell; it becomes even more prevalent in a dependently typed setting. Luckily, all is not lost: dependent types are expressive enough that they can talk about themselves reflectively, making meta-programming one of its potential killer applications with the potential of combining expressive types and reusable software components. Based on and inspired by recent research at Nottingham on dependently typed programming (EPSRC EP/C512022/1) and container types (EPSRCEP/C511964/2) and at Oxford on data type-generic programming (EPSRCGR/S27078/01, EP/E02128X/1) we plan to explore the potential of dependent types to deliver reusable and reliable software components. To achieve this, we intend to explore two alternative roads - reusability by structure and reusability by design - and express both within a dependently typed framework. Our programme is to build new tools extending the Epigram 2 framework, investigate the underlying theory using container types, and most importantly establish novel programming patterns and libraries. We seek funding for an RA at Nottingham (Peter Morris, whose PhD laid much of the groundwork for this proposal), and two doctoral students (one each at Oxford and Strathclyde), together with appropriate support for equipment, coordination, travel, and dissemination (i.e. a workshop and a summer school)
Period 01-Oct-2009 - 30-Sep-2013

more projects

Address

Computer and Information Sciences
Livingstone Tower

Location Map

View University of Strathclyde in a larger map