Follow
James McKinna
James McKinna
Verified email at hw.ac.uk
Title
Cited by
Cited by
Year
The view from the left
C McBride, J McKinna
Journal of functional programming 14 (01), 69-111, 2004
4322004
Pure type systems formalized
J McKinna, R Pollack
International Conference on Typed Lambda Calculi and Applications, 289-305, 1993
1721993
Some lambda calculus and type theory formalized
J McKinna, R Pollack
Journal of Automated Reasoning 23 (3), 373-409, 1999
154*1999
Inductive families need not store their indices
E Brady, C McBride, J McKinna
International Workshop on Types for Proofs and Programs, 115-129, 2003
1262003
Eliminating dependent pattern matching
H Goguen, C McBride, J McKinna
Algebra, Meaning, and Computation, 521-540, 2006
992006
Functional pearl: i am not a number--i am a free variable
C McBride, J McKinna
Proceedings of the 2004 ACM SIGPLAN workshop on Haskell, 1-9, 2004
942004
I am not a number: I am a free variable
C McBride, J McKinna
Proceedings of the ACM SIGPLAN Haskell Workshop, 2004
94*2004
Checking algorithms for pure type systems
LS van Benthem Jutting, J McKinna, R Pollack
Types for Proofs and Programs, 19-61, 1994
78*1994
Deliverables: a categorical approach to program development in type theory
J McKinna, R Burstall
Mathematical Foundations of Computer Science 1993, 32-67, 1993
761993
Deliverables: a categorical approach to program development in type theory
J McKinna, R Burstall
Mathematical Foundations of Computer Science 1993, 32-67, 1993
761993
Why dependent types matter
T Altenkirch, C McBride, J McKinna
Manuscript, available online, 235, 2005
702005
Why dependent types matter
J McKinna
ACM Sigplan Notices 41 (1), 1-1, 2006
682006
Type-and-scope safe programs and their proofs
G Allais, J Chapman, C McBride, J McKinna
ACM, New York, NY, 2017
532017
Certified Complexity (CerCo)
RM Amadio, N Ayache, F Bobot, JP Boender, B Campbell, I Garnier, ...
Foundational and Practical Aspects of Resource Analysis, 1-18, 2014
482014
A type-correct, stack-safe, provably correct, expression compiler in Epigram.
J Mckinna, J Wright
Submitted to the Journal of Functional Programming, 2006
41*2006
A type and scope safe universe of syntaxes with binding: their semantics and proofs
G Allais, R Atkey, J Chapman, C McBride, J McKinna
Proceedings of the ACM on Programming Languages 2 (ICFP), 1-30, 2018
372018
A few constructions on constructors
C McBride, H Goguen, J McKinna
Types for Proofs and Programs, 186-200, 2006
372006
Abstracting extensible data types: or, rows by any other name
JG Morris, J McKinna
Proceedings of the ACM on Programming Languages 3 (POPL), 1-28, 2019
342019
Proviola: A tool for proof re-animation
C Tankink, H Geuvers, J McKinna, F Wiedijk
International Conference on Intelligent Computer Mathematics, 440-454, 2010
322010
Towards a Repository of Bx Examples.
J Cheney, J McKinna, P Stevens, J Gibbons
EDBT/ICDT Workshops 1133, 87-91, 2014
282014
The system can't perform the operation now. Try again later.
Articles 1–20