Summary
Conor McBride (born 18 February 1973) is a Reader in the department of Computer and Information Sciences at the University of Strathclyde.[1] In 1999, he completed a Doctor of Philosophy (Ph.D.) in Dependently Typed Functional Programs and their Proofs[2] at the University of Edinburgh for his work in type theory.[3] He formerly worked at Durham University and briefly at Royal Holloway, University of London before joining the academic staff at the University of Strathclyde.
Conor McBride | |
|---|---|
| Born | 18 February 1973 |
| Alma mater | University of Edinburgh |
| Scientific career | |
| Fields | Computer science Type theory |
| Institutions | Durham University Royal Holloway, University of London University of Strathclyde |
| Thesis | Dependently Typed Functional Programs and their Proofs (1999) |
| Website | strictlypositive |
He was involved with developing international standards in programming and informatics, as a member of the International Federation for Information Processing (IFIP) IFIP Working Group 2.1 on Algorithmic Languages and Calculi,[4] which specified, maintains, and supports the programming languages ALGOL 60 and ALGOL 68.[5]
Research edit
His most notable research is in the field of type theory.[7] He cocreated the programming language Epigram with James McKinna.[8] Several of his articles, including the joint-written article defining the Epigram language, have been published in the Journal of Functional Programming.[9]
Selected bibliography edit
- with Dagand, Pierre-Evariste (2014). "Transporting Functions across Ornaments". ACM SIGPLAN Notices—ICFP. 47 (9): 103–114. arXiv:1201.4801. doi:10.1145/2398856.2364544.
- with Benton, Nick; Hur, Chung-Kil; Kennedy, Andrew J. (August 2012). "Strongly Typed Term representations in Coq" (PDF). Journal of Automated Reasoning. 49 (2): 141–159. CiteSeerX 10.1.1.296.8805. doi:10.1007/s10817-011-9219-0. S2CID 34005862.
- with Chapman, James; Dagand, Pierre-Evariste; Morris, Peter (September 2010). "The gentle art of levitation" (PDF). ACM SIGPLAN Notices—ICFP. 45 (9): 3–14. doi:10.1145/1932681.1863547.
- with Paterson, Ross (January 2008). "Applicative programming with effects" (PDF). Journal of Functional Programming. 18 (1). doi:10.1017/S0956796807006326.
- with Altenkirch, Thorsten; Morris, Peter (2007). "Generic Programming with Dependent Types" (PDF). Datatype-Generic Programming. Lecture Notes in Computer Science. Vol. 4719. pp. 209–257.
- with Altenkirch, Thorsten; McKinna, James. Why Dependent Types Matter (PDF).
- with Altenkirch, Thorsten, eds. (2007). Types for Proofs and Programs: International Workshop. Springer. ISBN 978-3540744634.
- – (2006). "A Few Constructions on Constructors". Types for Proofs and Programs. Lecture Notes in Computer Science. Vol. 3839. pp. 186–200. CiteSeerX 10.1.1.65.327.
- – (2005). "Epigram: Practical Programming with Dependent Types" (PDF). Advanced Functional Programming. Lecture Notes in Computer Science. Vol. 3622. pp. 130–170.
- with McKinna, James (January 2004). "The view from the left" (PDF). Journal of Functional Programming. 14 (1): 69–111. doi:10.1017/s0956796803004829. S2CID 6232997.
- with Abbott, Michael; Altenkirch, Thorsten; Ghani, Neil (2003). "Derivatives of Containers" (PDF). Proceedings of the 6th International Conference on Typed Lambda Calculi and Applications: 16–30.
- – (2002). "Elimination with a Motive" (PDF). Types for Proofs and Programs. Lecture Notes in Computer Science. Vol. 2277. pp. 197–216.
- – (2001). The Derivative of a Regular Type is its Type of One-Hole Contexts (PDF).
- – (2000). Dependently Typed Functional Programs and their Proofs (PDF). University of Edinburgh College of Science and Engineering.
Video lectures edit
- McBride, Conor (3 February 2011). Dependently Typed Programming: An Agda Introduction (first of 15 lectures) (video). Iain McGinniss.
- McBride, Conor (10 September 2012). ICFP 2012 Monday keynote. Conor McBride: Agda-curious? (video). Malcolm Wallace.
References edit
- ^ "Dr Conor McBride: Reader: Computer and Information Sciences". University of Strathclyde: Computer and Information Sciences.
- ^ McBride, Conor (July 2000). "Dependently Typed Functional Programs and their Proofs". Edinburgh Research Archive. University of Edinburgh. hdl:1842/374. Retrieved 15 January 2016.
- ^ McBride, Conor (1999). "Dependently Typed Functional Programs and their Proofs" (PDF). University of Edinburgh.
- ^ Jeuring, Johan; Meertens, Lambert; Guttmann, Walter (17 August 2016). "Profile of IFIP Working Group 2.1". Foswiki. Retrieved 16 October 2020.
- ^ Swierstra, Doaitse; Gibbons, Jeremy; Meertens, Lambert (2 March 2011). "ScopeEtc: IFIP21: Foswiki". Foswiki. Retrieved 16 October 2020.
- ^ McBride, Conor. "Conor's Staring out the Window". Computer & Information Sciences. University of Strathclyde. Retrieved 18 August 2020.
- ^ Altenkirch, Thorsten; McBride, Conor. "Towards Observational Type Theory" (PDF). StrictlyPositive.org.
- ^ McBride, Conor; McKinna, James (January 2004). "The view from the left". Journal of Functional Programming. 14 (1): 69–111. doi:10.1017/s0956796803004829. S2CID 6232997.
- ^ Cambridge Journals Online: Journal of Functional Programming, Conor McBride
External links edit
- Official website, University of Strathclyde
- Official website, personal
- Conor McBride at the Mathematics Genealogy Project
- Conor McBride at DBLP Bibliography Server
