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
3892004
Pure type systems formalized
J McKinna, R Pollack
International Conference on Typed Lambda Calculi and Applications, 289-305, 1993
1611993
Some lambda calculus and type theory formalized
J McKinna, R Pollack
Journal of Automated Reasoning 23 (3), 373-409, 1999
150*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
1072003
Eliminating dependent pattern matching
H Goguen, C McBride, J McKinna
Algebra, Meaning, and Computation, 521-540, 2006
852006
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
842004
I am not a number: I am a free variable
C McBride, J McKinna
Proceedings of the ACM SIGPLAN Haskell Workshop, 2004
84*2004
Checking algorithms for pure type systems
LS van Benthem Jutting, J McKinna, R Pollack
Types for Proofs and Programs, 19-61, 1994
76*1994
Why dependent types matter
T Altenkirch, C McBride, J McKinna
Manuscript, available online, 235, 2005
692005
Why dependent types matter
J McKinna
ACM Sigplan Notices 41 (1), 1-1, 2006
642006
Deliverables: a categorical approach to program development in type theory
J McKinna, R Burstall
Mathematical Foundations of Computer Science 1993, 32-67, 1993
631993
Deliverables: a categorical approach to program development in type theory
J McKinna, R Burstall
Mathematical Foundations of Computer Science 1993, 32-67, 1993
631993
Type-and-scope safe programs and their proofs
G Allais, J Chapman, C McBride, J McKinna
ACM, New York, NY, 2017
392017
A few constructions on constructors
C McBride, H Goguen, J McKinna
Types for Proofs and Programs, 186-200, 2006
352006
A type-correct, stack-safe, provably correct, expression compiler in Epigram.
J Mckinna, J Wright
Submitted to the Journal of Functional Programming, 2006
32*2006
Proviola: A tool for proof re-animation
C Tankink, H Geuvers, J McKinna, F Wiedijk
International Conference on Intelligent Computer Mathematics, 440-454, 2010
302010
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
292014
Towards a Repository of Bx Examples.
J Cheney, J McKinna, P Stevens, J Gibbons
EDBT/ICDT Workshops 1133, 87-91, 2014
252014
A Focused Sequent Calculus Framework for Proof Search in Pure Type Systems
J McKinna, R Dyckhoff, SJE Lengrand
Logical Methods in Computer Science 7, 2011
24*2011
A focused sequent calculus framework for proof search in Pure Type Systems
SJE Lengrand, R Dyckhoff, J McKinna
arXiv preprint arXiv:1012.3372, 2010
242010
The system can't perform the operation now. Try again later.
Articles 1–20