James McKinna
James McKinna
Verified email at ed.ac.uk
TitleCited byYear
The view from the left
C McBride, J McKinna
Journal of functional programming 14 (01), 69-111, 2004
3812004
Pure type systems formalized
J McKinna, R Pollack
International Conference on Typed Lambda Calculi and Applications, 289-305, 1993
1541993
Some lambda calculus and type theory formalized
J McKinna, R Pollack
Journal of Automated Reasoning 23 (3), 373-409, 1999
144*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
1002003
Checking algorithms for pure type systems
LS van Benthem Jutting, J McKinna, R Pollack
Types for Proofs and Programs, 19-61, 1994
77*1994
Eliminating dependent pattern matching
H Goguen, C McBride, J McKinna
Algebra, Meaning, and Computation, 521-540, 2006
752006
Why dependent types matter
T Altenkirch, C McBride, J McKinna
Manuscript, available online, 235, 2005
692005
Deliverables: a categorical approach to program development in type theory
J McKinna, R Burstall
Mathematical Foundations of Computer Science 1993, 32-67, 1993
671993
Deliverables: a categorical approach to program development in type theory
J McKinna, R Burstall
Mathematical Foundations of Computer Science 1993, 32-67, 1993
671993
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
652004
Why dependent types matter
J McKinna
ACM Sigplan Notices 41 (1), 1-1, 2006
622006
A few constructions on constructors
C McBride, H Goguen, J McKinna
Types for Proofs and Programs, 186-200, 2006
342006
Proviola: A tool for proof re-animation
C Tankink, H Geuvers, J McKinna, F Wiedijk
International Conference on Intelligent Computer Mathematics, 440-454, 2010
292010
A type-correct, stack-safe, provably correct, expression compiler in Epigram.
J Mckinna, J Wright
Submitted to the Journal of Functional Programming, 2006
29*2006
Towards a Repository of Bx Examples.
J Cheney, J McKinna, P Stevens, J Gibbons
EDBT/ICDT Workshops 1133, 87-91, 2014
232014
Type-and-scope safe programs and their proofs
G Allais, J Chapman, C McBride, J McKinna
ACM, New York, NY, 2017
212017
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
202014
A focused sequent calculus framework for proof search in Pure Type Systems
SJE Lengrand, R Dyckhoff, J McKinna
arXiv preprint arXiv:1012.3372, 2010
202010
Deliverables: an approach to program development in the calculus of constructions
RM Burstall, J McKinna
LFCS, Department of Computer Science, University of Edinburgh, 1991
201991
Towards a Principle of Least Surprise for Bidirectional Transformations.
J Cheney, J Gibbons, J McKinna, P Stevens
Bx@ STAF, 66-80, 2015
162015
The system can't perform the operation now. Try again later.
Articles 1–20