James McKinna

	2012
21		Herman Geuvers, Robbert Krebbers, James McKinna: The lambda-mu-T-calculus CoRR abs/1204.0347: (2012)
	2011
20		Stéphane Lengrand, Roy Dyckhoff, James McKinna: A Focused Sequent Calculus Framework for Proof Search in Pure Type Systems Logical Methods in Computer Science 7(1): (2011)
	2010
19		Carst Tankink, Herman Geuvers, James McKinna, Freek Wiedijk: Proviola: A Tool for Proof Re-animation. AISC/MKM/Calculemus 2010: 440-454
18		Herman Geuvers, Robbert Krebbers, James McKinna, Freek Wiedijk: Pure Type Systems without Explicit Contexts LFMTP 2010: 53-67
17		Carst Tankink, Herman Geuvers, James McKinna, Freek Wiedijk: Proviola: A Tool for Proof Re-animation CoRR abs/1005.2672: (2010)
	2009
16		Lionel Elie Mamane, Herman Geuvers, James McKinna: A Logically Saturated Extension of lambdaµµ. Calculemus/MKM 2009: 405-421
15		Saleem Bhatti, Edwin Brady, Kevin Hammond, James McKinna: Domain Specific Languages (DSLs) for Network Protocols (Position Paper). ICDCS Workshops 2009: 208-213
	2008
14		Peter Chapman, James McKinna, Christian Urban: Mechanising a Proof of Craig's Interpolation Theorem for Intuitionistic Logic in Nominal Isabelle. AISC/MKM/Calculemus 2008: 38-52
13		Cezary Kaliszyk, Pierre Corbineau, Freek Wiedijk, James McKinna, Herman Geuvers: A Real Semantic Web for Mathematics Deserves a Real Semantics. SemWiki 2008
12		Eelis van der Weegen, James McKinna: A Machine-Checked Proof of the Average-Case Complexity of Quicksort in Coq. TYPES 2008: 256-271
	2006
11		Stéphane Lengrand, Roy Dyckhoff, James McKinna: A Sequent Calculus for Type Theory. CSL 2006: 441-455
10		Healfdene Goguen, Conor McBride, James McKinna: Eliminating Dependent Pattern Matching. Essays Dedicated to Joseph A. Goguen 2006: 521-540
9		James McKinna: Why dependent types matter. POPL 2006: 1
	2004
8		Conor McBride, Healfdene Goguen, James McKinna: A Few Constructions on Constructors. TYPES 2004: 186-200
7		Conor McBride, James McKinna: The view from the left. J. Funct. Program. 14(1): 69-111 (2004)
	2003
6		Edwin Brady, Conor McBride, James McKinna: Inductive Families Need Not Store Their Indices. TYPES 2003: 115-129
	2002
5		Paul Callaghan, Zhaohui Luo, James McKinna, Robert Pollack: Types for Proofs and Programs, International Workshop, TYPES 2000, Durham, UK, December 8-12, 2000, Selected Papers Springer 2002
	1999
4		James McKinna, Robert Pollack: Some Lambda Calculus and Type Theory Formalized. J. Autom. Reasoning 23(3-4): 373-409 (1999)
	1993
3		James McKinna, Rod M. Burstall: Deliverables: A Categorial Approach to Program Development in Type Theory. MFCS 1993: 32-67
2		James McKinna, Robert Pollack: Pure Type Systems Formalized. TLCA 1993: 289-305
1		L. S. van Benthem Jutting, James McKinna, Robert Pollack: Checking Algorithms for Pure Type Systems. TYPES 1993: 19-61

Coauthor Index

1	Saleem N. Bhatti (Saleem Bhatti)	[15]
2	Edwin Brady	[6] [15]
3	Rod M. Burstall	[3]
4	Paul Callaghan	[5]
5	Peter Chapman	[14]
6	Pierre Corbineau	[13]
7	Roy Dyckhoff	[11] [20]
8	Herman Geuvers	[13] [16] [17] [18] [19] [21]
9	Healfdene Goguen	[8] [10]
10	Kevin Hammond	[15]
11	L. S. van Benthem Jutting	[1]
12	Cezary Kaliszyk	[13]
13	Robbert Krebbers	[18] [21]
14	Stéphane Lengrand	[11] [20]
15	Zhaohui Luo	[5]
16	Lionel Elie Mamane	[16]
17	Conor McBride	[6] [7] [8] [10]
18	Robert Pollack	[1] [2] [4] [5]
19	Carst Tankink	[17] [19]
20	Christian Urban	[14]
21	Eelis van der Weegen	[12]
22	Freek Wiedijk	[13] [17] [18] [19]

Colors in the list of coauthors

Last update Sun Jun 3 16:06:10 2012 CET by the DBLP Team — Data released under the ODC-BY 1.0 license — See also our legal information page