If you made any changes in Pure these will be visible here soon.

Research Output

Article

Applicative programming with effects

Mcbride, C. & Paterson, R., 2008, In : Journal of Functional Programming. 18, 1, p. 1-13 13 p.

Research output: Contribution to journalArticle

228 Citations (Scopus)

A tutorial implementation of a dependently typed lambda calculus

Löh, A., Mcbride, C. & Swierstra, W., 2010, In : Fundamenta Informaticae. 102, 2, p. 177-207 31 p.

Research output: Contribution to journalArticle

11 Citations (Scopus)

A type and scope safe universe of syntaxes with binding: their semantics and proofs

Allais, G., Atkey, R., Chapman, J., McBride, C. & McKinna, J., 28 Jan 2020, (Accepted/In press) In : Journal of Functional Programming. 61 p.

Research output: Contribution to journalArticle

Preface

McBride, C. & Uustalu, T., May 2009, In : Journal of Functional Programming. 19, 3-4, p. 263-264 1 p.

Research output: Contribution to journalArticle

Strongly typed term representations in Coq

Benton, N., Hur, C-K., Kennedy, A. & McBride, C., Aug 2012, In : Journal of Automated Reasoning. 49, 2, p. 141-159 19 p.

Research output: Contribution to journalArticle

28 Citations (Scopus)

Transporting functions across ornaments

Dagand, P-É. & McBride, C., 30 May 2014, In : Journal of Functional Programming. 24, 2-3, p. 316-383 68 p.

Research output: Contribution to journalArticle

Open Access
File
5 Citations (Scopus)
17 Downloads (Pure)
Book

A List of Successes That Can Change the World: Essays Dedicated to Philip Wadler on the Occasion of His 60th Birthday

Lindley, S. (ed.), McBride, C. (ed.), Trinder, P. (ed.) & Sannella, D. (ed.), 25 Mar 2016, Springer. 478 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 9600)

Research output: Book/ReportBook

Chapter

Let's see how things unfold.: reconciling the infinite with the intensional (extended abstract)

McBride, C., Kurz, A. (ed.), Lenisa, M. (ed.) & Tarlecki, A. (ed.), Sep 2009, Algebra and Coalgebra in Computer Science. 5728 ed. Springer, p. 113-126 13 p. (Lecture Notes in Computer Science).

Research output: Chapter in Book/Report/Conference proceedingChapter

12 Citations (Scopus)
Conference Contribution

Everybody's got to be somewhere

McBride, C., 10 Jul 2018, In : Electronic Proceedings in Theoretical Computer Science. 275, p. 53-69 17 p.

Research output: Contribution to journalConference Contribution

Open Access
File
3 Citations (Scopus)
39 Downloads (Pure)
Conference contribution book

Clowns to the left of me, jokers to the right (pearl): dissecting data structures

Mcbride, C., 2008, POPL '08 Proceedings of the 35th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages . p. 287-295 9 p.

Research output: Chapter in Book/Report/Conference proceedingConference contribution book

10 Citations (Scopus)

Do Be Do Be Do

Lindley, S., McBride, C. & McLaughlin, C., 15 Jan 2017, POPL'2017 : Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages. Gordon, A. (ed.). New York, p. 500-514 15 p.

Research output: Chapter in Book/Report/Conference proceedingConference contribution book

Open Access
File
19 Citations (Scopus)
184 Downloads (Pure)

How to keep your neighbours in order

McBride, C., 19 Aug 2014, ICFP '14 Proceedings of the 19th ACM SIGPLAN International Conference on Functional Programming. New York, NY., p. 297-309 14 p.

Research output: Chapter in Book/Report/Conference proceedingConference contribution book

Open Access
File
31 Downloads (Pure)

I got plenty o’ nuttin’

McBride, C., 25 Mar 2016, A List of Successes That Can Change the World: Essays Dedicated to Philip Wadler on the Occasion of His 60th Birthday. Lindley, S., McBride, C., Trinder, P. & Sannella, D. (eds.). Switzerland: Springer, p. 207-233 27 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 9600).

Research output: Chapter in Book/Report/Conference proceedingConference contribution book

12 Citations (Scopus)

Outrageous but meaningful coincidences: dependent type-safe syntax and evaluation

Mcbride, C., 2010, Proceedings of the 6th ACM SIGPLAN workshop on Generic programming . New York, p. 1-12 12 p.

Research output: Chapter in Book/Report/Conference proceedingConference contribution book

18 Citations (Scopus)

Productive coprogramming with guarded recursion

Atkey, R. & McBride, C., Sep 2013, (Accepted/In press) Proceedings of the 2013 ACM SIGPLAN International Conference on Functional Programming . 12 p.

Research output: Chapter in Book/Report/Conference proceedingConference contribution book

23 Citations (Scopus)

Small induction recursion

Hancock, P., McBride, C., Ghani, N., Malatesta, L. & Altenkirch, T., 6 Jun 2013, Typed Lambda Calculus and Applications: 11th International Conference, TLCA 2013, Eindhoven, The Netherlands, June 26-28, 2013. Proceedings. Hasegawa, M. (ed.). Berlin: Springer, p. 156-172 17 p. (Lecture Notes in Computer Science; vol. 7941).

Research output: Chapter in Book/Report/Conference proceedingConference contribution book

9 Citations (Scopus)

The gentle art of levitation

Chapman, J., Dagand, P-E., Mcbride, C. & Morris, P., 2010, ICFP 2010 Proceedings of the 15th ACM SIGPLAN international conference on functional programming. Hudak, P. (ed.). New York, p. 3-14 12 p.

Research output: Chapter in Book/Report/Conference proceedingConference contribution book

20 Citations (Scopus)

Transporting functions across ornaments

Dagand, P-E. & McBride, C., 2012, ICFP '12 Proceedings of the 17th ACM SIGPLAN international conference on Functional programming . New York, p. 104-113 10 p.

Research output: Chapter in Book/Report/Conference proceedingConference contribution book

14 Citations (Scopus)

Turing-completeness totally free

McBride, C., 9 Jun 2015, Mathematics of Program Construction: 12th International Conference, MPC 2015, Königswinter, Germany, June 29--July 1, 2015. Proceedings. Hinze, R. & Voigtländer, J. (eds.). Cham, Switzerland: Springer, Vol. 9129. p. 257-275 19 p. (Lecture Notes in Computer Science; vol. 9129).

Research output: Chapter in Book/Report/Conference proceedingConference contribution book

Open Access
File
9 Citations (Scopus)
33 Downloads (Pure)

Type-and-scope safe programs and their proofs

Allais, G., Chapman, J., McBride, C. & McKinna, J., 16 Jan 2017, CPP 2017 : Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs. Bertot, Y. & Vafeiadis, V. (eds.). New York, 13 p.

Research output: Chapter in Book/Report/Conference proceedingConference contribution book

Open Access
File
14 Citations (Scopus)
80 Downloads (Pure)

Type inference in context

Gundry, A., Mcbride, C. & McKinna, J., 2010, MSFP '10 Proceedings of the third ACM SIGPLAN workshop on Mathematically structured functional programming . p. 43-54 12 p.

Research output: Chapter in Book/Report/Conference proceedingConference contribution book

3 Citations (Scopus)

Variations on inductive-recursive definitions

Ghani, N., McBride, C., Nordvall Forsberg, F. & Spahn, S., 30 Nov 2017, Proceedings of the 42nd International Symposium on Mathematical Foundations of Computer Science. Germany, 13 p. 63. (Leibniz International Proceedings in Informatics ).

Research output: Chapter in Book/Report/Conference proceedingConference contribution book

Open Access
File
22 Downloads (Pure)
Paper

A type and scope safe universe of syntaxes with binding: their semantics and proofs

Allais, G., Atkey, R., Chapman, J., McBride, C. & McKinna, J., 23 Sep 2018. 30 p.

Research output: Contribution to conferencePaper

Open Access
File
58 Downloads (Pure)