Selected Publications                (Books listed elsewhere)

• Access control and privacy policy
  • Privacy policy languages and enforcement
  • Access control (Trust management and the RT system)
• Web security, authentication, and identity theft
• Distributed mechanism design
• Network Protocols and Security Analysis
• Finite-state analysis and case studies (including 802.11i wireless authentication, SSL, contract signing)
• Protocol composition logic
• Logical methods, decision procedures, and lower bounds
• Probabilistic polynomial-time process calculus for asymptotic security analysis
• Universal composability, reactive simulatability, and related approaches
• Malware detection and mitigation
• Mobile code securty
• Hardware support for tamper-resistant code
• Pre-2000 work on programming languages, type systems, linear logic, and semantics
• Object systems
• Linear logic
• Type theory and semantics
• Other

Recent papers not sorted by topic (2008-2010)

• D. Akhawe, A. Barth, P. Lam, J.C. Mitchell and D. Song, Towards a formal foundation of Web security, Proc. IEEE Symposium on Computer Security Foundations, July 2010.
• S. Maffeis, J.C. Mitchell and A. Taly, Object Capabilities and Isolation of Untrusted Web Applications, Proc. IEEE Symposium on Security and Privacy, May 2010. ( longer version)
• J. Bau, E. Bursztein, D. Gupta, J.C. Mitchell State of the Art: Automated Black-Box Web Application Vulnerability Testing, Proc. IEEE Symposium on Security and Privacy, May 2010.
• E. Bursztein, S. Bethard, J.C. Mitchell, D. Jurafsky, C. Fabry How Good are Humans at Solving CAPTCHAs? A Large Scale Evaluation Proc. IEEE Symposium on Security and Privacy, May 2010.
• J. Bau and J.C. Mitchell, A Security Evaluation of DNSSEC with NSEC3, Network and Distributed Systems Security (NDSS), 2010.
• A.Barth, B. Rubinstein, M. Sundararajan, J.C. Mitchell, D. Song, and P.L. Bartlett, A Learning-Based Approach to Reactive Security, Proc. of the 14th International Conference on Financial Cryptography and Data Security (FC 2010), 2010.
• E. Bursztein, J.C. Mitchell, Using Strategy Objectives for Network Security Analysis, Inscrypt'09, December 2009.
• E. Bursztein, P.E. Lam, J.C. Mitchell, TrackBack Spam: Abuse and Prevention, Proc. ACM Cloud Computing Security Workshop, Chicago, November, 2009.
• S. Maffeis, J.C. Mitchell and A. Taly, Isolating JavaScript with Filters, Rewriting, and Wrappers, 14th European Symposium on Research in Computer Security (ESORICS), Saint Malo, France, September 21-25, 2009.
• P.F. Lam, J.C. Mitchell, and S. Sundaram, A Formalization of HIPAA for a Medical Messaging System, 6th International Conference on Trust, Privacy \& Security in Digital Business (TrustBus'09), 2009.
• T. Hinrichs, N. Gude. M. Casado, J.C. Mitchell, S. Shenker, Practical Declarative Network Management, ACM SIGCOMM Workshop: Research on Enterprise Networking (WREN 2009), 2009.
• S. Maffeis, J.C. Mitchell and A. Taly, Run-Time Enforcement of Secure JavaScript Subsets, Web 2.0 Security and Privacy (W2SP'09), 2009.
• S. Maffeis, (J.C. Mitchell) and A. Taly, Language-Based Isolation of Untrusted JavaScript (later tech report), IEEE Symp. Computer Security Foundations (CSF'09), 2009.
• S. Maffeis, J.C. Mitchell and A. Taly, An Operational Semantics for Javascript, ASIAN Symposium on Programming Languages and Systems (APLAS), 2008.
• A. Barth, C. Jackson, and J.C. Mitchell, Robust Defenses for Cross-Site Request Forgery, Proc. 15th ACM Conference on Computer and Communications Security (CCS 2008), 2008.
• E. Stinson, J.C. Mitchell, Towards Systematic Evaluation of the Evadability of Bot/Botnet Detection Methods, 2nd USENIX Workshop on Offensive Technologies (WOOT '08), 2008.
• L. Martignoni, E. Stinson, M Fredrikson, S. Jha, J.C. Mitchell, A Layered Architecture for Detecting Malicious Behaviors, 11th Int'l Symp. Recent Advances In Intrusion Detection (RAID), 2008.
• A. Barth, C. Jackson, and J.C. Mitchell, Securing Frame Communication in Browsers, Proc. of the 17th USENIX Security Symposium. (USENIX Security 2008), 2008. ( CACM version)
• J.C. Mitchell, A. Roy, P. Rowe, A. Scedrov, Analysis of EAP-GPSK Authentication Protocol, Applied Cryptography and Network Security, 2008.
• A. Miura-Ko, B. Yolken, J.C. Mitchell and N. Bambos, Security decision-making among interdependent organizations, IEEE Computer Security Foundations (CSF), 2008.

Access Control and Privacy Policy

Privacy policy languages and enforcement

• A. Barth, A. Datta, J.C. Mitchell, and S. Sundaram, Privacy and Utility in Business Processes, 20th IEEE Computer Security Foundations Symposium (CSF 20), Venice, July, 2007.
• A. Barth, A. Datta, J. C. Mitchell, and H. Nissenbaum, Privacy and Contextual Integrity: Framework and Applications, Proceedings of 27th IEEE Symposium on Security and Privacy, May 2006.
• A. Barth and J.C. Mitchell, Enterprise privacy promises and enforcement, Workshop on Issues in the Theory of Security (WITS'05), San Diego, January, 2005.
• A. Barth, J.C. Mitchell, and J. Rosenstein, Conflict and Combination in Privacy Policy Languages, Workshop on Privacy in the Electronic Society (WPES), Washington (DC), October, 2004.

Access control (including DRM, Trust management and the RT system)

• A. Barth and J.C. Mitchell, Managing Digital Rights using Linear Logic, Proc 21st Annual IEEE Symposium on Logic in Computer Science. 2006.
• N. Li and J.C. Mitchell, Understanding SPKI/SDSI using first-order logic. Int. J. Inf. Sec. 5(1): 48-64 (2006).
• N. Li, J.C. Mitchell, and W.H. Winsborough, Beyond Proof-of-compliance: Security Analysis in Trust Management, J. ACM, Vol. 52, pp 474-514, 2005.
• A. Chander, D. Dean, and J.C. Mitchell, Reconstructing Trust Management, Journal of Computer Security, vol 12, number 1, 2004, pages 131-164.
• N. Li and J.C. Mitchell, Understanding SPKI/SDSI Using First-Order Logic, IEEE Computer Security Foundations Workshop, Pacific Grove, California, June 2003, pages 89-103.
• N. Li, J.C. Mitchell, and W.H. Winsborough, Beyond Proof-of-compliance: Safety and Availability Analysis in Trust Management, IEEE Symp. on Security and Privacy, Oakland, May 2003.
• N. Li and J.C. Mitchell, RT: A Role-based Trust-management Framework, DARPA Information Survivability Conference and Exposition (DISCEX III), April, 2003.
• N. Li, W. Winsborough, J.C. Mitchell, Distributed Credential Chain Discovery in Trust Management, J. Computer Security, vol 11, no 1, 2003, pages 35-86.
• N. Li and J.C. Mitchell, Datalog with Constraints: A Foundation for Trust-management Languages, Proc. Fifth International Symposium on Practical Aspects of Declarative Languages (PADL 2003), New Orleans, Louisiana, Springer LNCS Vol. 2562, January 2003, pp. 58-73.
• N. Li, J.C. Mitchell, W.H. Winsborough, Design of a Role-based Trust-management Framework, IEEE Symp. on Security and Privacy, Oakland, May 2002.
• N. Li, W.H. Winsborough, and J.C. Mitchell, Distributed Credential Chain Discovery in Trust Management (Extended Abstract), Proc. 8th ACM Conference on Computer and Communications Security, pages 156-165. ACM Press, November 2001.
• A. Chander, D. Dean, J.C. Mitchell, Deconstructing Trust Management, ACM SIGPLAN and IFIP WG 1.7 Workshop on Issues in the Theory of Security (WITS'02) Portland, Oregon, USA, January 14-15, 2002. Electronic proceedings
• A. Chander, D. Dean, and J.C. Mitchell, A state-transition model of trust management and access control, 14th IEEE Computer Security Foundations Workshop, Cape Breton, Nova Scotia, June 11-13, 2001.

Web Security, Authentication, and Identity Theft

• C. Jackson, D. Boneh, and J.C Mitchell. Transaction Generators: Rootkits for the Web, 2nd USENIX Workshop on Hot Topics in Security (HotSec '07). (Also: Spyblock site.)
• C. Jackson, D. Boneh, and J.C. Mitchell, Protecting Browser State from Web Privacy Attacks, 15th International World Wide Web Conference (WWW 2006), Edinburgh, May, 2006.
(Also: SafeHistory and SafeCache browser extension sites.)
• B. Ross, C. Jackson, N. Miyake, D. Boneh, and J.C, Mitchell, Stronger Password Authentication Using Browser Extensions, Usenix Security Symposium, Baltimore, August, 2005.
(Also: PwdHash site.)
• N. Chou, R. Ledesma, Y. Teraguchi, D.Boneh, and J.C. Mitchell, Client-Side Defense Against Web-Based Identity Theft, 11th Annual Network and Distributed System Security Symposium (NDSS '04), San Diego, February, 2004.

Distributed Mechanism Design

• J.C. Mitchell and V. Teague, Autonomous Nodes and Distributed Mechanisms, in M. Okada, B. Pierce, A. Scedrov, H. Tokuda, and A. Yonezawa (eds.), Software Security - Theories and Systems. Mext-NSF-JSPS International Symposium, ISSS 2002,  Tokyo, Japan, November 8-10, 2002,  Springer LNCS Volume 2609, Springer-Verlag, 2003, pp. 58-83.

Network Protocols and Security Analysis

Finite-state analysis and case studies (including 802.11i wireless authentication, SSL, contract signing)

• C. He and J.C. Mitchell, Security Analysis and Improvements for IEEE 802.11i, Network and Distributed System Security Symposium (NDSS '05), San Diego, February, 2005.
• C. He and J.C. Mitchell, Analysis of the 802.11i 4-Way Handshake, ACM Workshop on Wireless Security (WiSe 2004), Philadelphia, October, 2004.
• V. Shmatikov and J.C. Mitchell, Finite-State Analysis of Two Contract Signing Protocols, Theoretical Computer Science, 283, June 2002, pages 419-450.
• V. Shmatikov and J.C. Mitchell, Analysis of Abuse-Free Contract Signing, Financial Cryptography ’00, Anguilla, 2000.
• V. Shmatikov and J.C. Mitchell, Analysis of a Fair Exchange Protocol, Seventh Annual Symposium on Network and Distributed System Security (NDSS 2000), San Diego, 2000, pages 119-128.
• J.C. Mitchell, V.Shmatikov, and U. Stern, Finite-State Analysis of SSL 3.0, Seventh USENIX Security Symposium, San Antonio, 1998, pages 201-216. Preliminary version presented at DIMACS Workshop on Design and Formal Verification of Security Protocols, September 1997, and distributed on workshop CD.
• J.C. Mitchell, M. Mitchell, and U.Stern, Automated Analysis of Cryptographic Protocols Using Murphi, IEEE Symp. Security and Privacy, Oakland, 1997, pages 141-153.

Protocol composition logic

• A. Roy, A. Datta, and J.C. Mitchell, Formal Proofs of Cryptographic Security of Diffie-Hellman based Protocols, Proc. Symposium On Trustworthy Global Computing, Springer LNCS, November 2007.
• A. Roy, A. Datta, A. Derek, and J.C. Mitchell, Inductive Proofs of Computational Secrecy, Proc. 12th European Symposium On Research In Computer Security, September, 2007.
• A. Roy, A. Datta, A. Derek, J.C. Mitchell, and J-P Seifert, Secrecy Analysis in Protocol Composition Logic. In Formal Logical Methods for System Security and Correctness, IOS Press, 2008. Volume based on presentations at Summer School 2007, Formal Logical Methods for System Security and Correctness, Marktoberdorf, Germany.
• A. Roy, A. Datta, A. Derek and J.C. Mitchell. Inductive Trace Properties Imply Computational Security, 7th International Workshop on Issues in the Theory of Security (WITS'07), Braga, Portugal, March, 2007.
• A. Datta, A. Derrick, J.C. Mitchell and A. Roy, Protocol composition logic (PCL). In Computation, Meaning and Logic: Articles dedicated to Gordon Plotkin, ed. L. Cardelli, M. Fiore and G. Winskel, Electronic Notes in Theoretical Computer Science, 2007.
• C. He, M. Sundararajan, A. Datta, A. Derek, and J. C. Mitchell, A Modular Correctness Proof of TLS and IEEE 802.11i, ACM Transactions on Information and System Security,accepted for publication.
• A. Roy, A. Datta, A. Derek, J.C.~Mitchell, and J.-P. Seifert, Secrecy Analysis in Protocol Composition Logic, 11th Annual Asian Computing Science Conference (ASIAN'06), Tokyo, December, 2006.
• M. Backes, A. Datta, A. Derek, J. C. Mitchell, and M. Turuani, Compositional Analysis of Contract-Signing Protocols, Theor. Comput. Sci. 367(1-2): 33-56 (2006)
• A. Datta, A. Derek, J.C. Mitchell, and B. Warinschi, Key Exchange Protocols: Security Definition, Proof Method, and Applications, 19th IEEE Computer Security Foundations Workshop (CSFW 19), Venice, July, 2006.
• C. He, M. Sundararajan, A. Datta, A. Derek, and J. C. Mitchell, A Modular Correctness Proof of TLS and IEEE 802.11i, ACM Conference on Computer and Communications Security (CCS '05), November, 2005.
• A. Datta, A. Derek, J.C. Mitchell, V. Shmatikov, and M. Turuani, Probabilistic polynomial-time semantics for a protocol security logic, 32nd International Colloquium on Automata, Languages and Programming (ICALP '05), Lisbon, July, 2005.
• M. Backes, A. Datta, A. Derek, J.C. Mitchell, and M. Turuani, Compositional Analysis of Contract Signing Protocols, 18th IEEE Computer Security Foundations Workshop (CSFW '05), June, 2005.
• A. Datta, A. Derek, J. C. Mitchell, and D. Pavlovic, A Derivation System and Compositional Logic for Security Protocols, Journal of Computer Security (Special Issue of Selected Papers from CSFW-16), Vol 13, 2005, pages 423–482.
• A. Datta and A. Derek and J. C. Mitchell and D. Pavlovic, Abstraction and Refinement in Protocol Derivation, IEEE Computer Security Foundations Workshop, Pacific Grove, California, June 2004.
• A. Datta and A. Derek and J. C. Mitchell and D. Pavlovic, Secure protocol composition, Proc. of Mathematical Foundations of Programming Semantics, Electronic Notes in Theoretical Computer Science, vol 83, 2003.
• A. Datta, A. Derek, J. C. Mitchell, and D. Pavlovic, Secure protocol composition (Extended abstract), Proc. ACM Workshop on Formal Methods in Security Engineering, 2003, pages 11-23.
• A. Datta, A. Derek, J.C. Mitchell, and D. Pavlovic, A Derivation System for Security Protocols and its Logical Formalization, IEEE Computer Security Foundations Workshop, Pacific Grove, California, June 2003, pages 109-125.
• N.A. Durgin, J.C. Mitchell, and D. Pavlovic, A compositional logic for proving security properties of protocols, Journal of Computer Security, vol 11, number 4, 2003, pages 677-721.
• N.A. Durgin, J.C. Mitchell, and D. Pavlovic, A Compositional Logic for Protocol Correctness, 14th IEEE Computer Security Foundations Workshop, Cape Breton, Nova Scotia,  June 11-13, 2001.

Probabilistic Foundations, Ideal Functionality and specification methods

• R. Kuesters, A. Datta, J.C. Mitchell, and A. Ramanathan, On the Relationships Between Notions of Simulation-Based Security, J. Cryptology, accepted for publication.
• J.C. Mitchell, A. Ramanathan, A Scedrov, and V. Teague, A probabilistic polynomial-time process calculus for the analysis of cryptographic protocols, Theoretical Computer Science 353 (2006) 118--164.
• A. Datta, A. Derek, J.C. Mitchell, A. Ramanathan, and A. Scedrov, Games and the Impossibility of Realizable Ideal Functionality, Theory of Cryptography Conference (TCC), 2006.
• A. Datta, R. Kuesters, J. C. Mitchell, A. Ramanathan, On the Relationships between Notions of Simulation-based Security, in Proceedings of Theory of Cryptography Conference, Lecture Notes in Computer Science, Vol. 3378, pp. 476-494, February 2005.
• A. Datta, R. Kuesters, J.C. Mitchell, A. Ramanathan, V. Shmatikov, Unifying Equivalence-Based Definitions of Protocol Security, Workshop on Issues in the Theory of Security (WITS'04), Barcelona, April, 2004.
• A. Ramanathan, J.C. Mitchell, A. Scedrov, and V. Teague, Probabilistic bisimulation and equivalence for security analysis of network protocols, Foundations of Software Science and Computation Structures (FOSSACS 2004), Barcelona, March, 2004.
• P. Mateus, J.C. Mitchell, and A. Scedrov, Composition of Cryptographic Protocols in a Probabilistic Polynomial-Time Calculus, CONCUR 2003, Marseille, France, Springer LNCS Volume 2761, Springer-Verlag, 2003, pp. 327-349.
• J. Mitchell, A. Ramanathan, A. Scedrov, and V. Teague, A probabilistic polynomial-time calculus for analysis of cryptographic protocols (Preliminary report), 17-th Annual Conference on the Mathematical Foundations of Programming Semantics, Arhus, Denmark, May, 2001, Electronic Notes in Theoretical Computer Science, Volume 45 (2001).
• Lincoln,P.D., Mitchell, J.C., Mitchell, M., and Scedrov, A., Probabilistic polynomial-time equivalence and security protocols, FM'99 World Congress On Formal Methods in the Development of Computing Systems, Toulouse, France, September, 1999.
• Lincoln, P.D., Mitchell, J.C., Mitchell, M. and Scedrov, A., A Probabilistic Poly-time Framework for Protocol Analysis, ACM Computer and Communication Security (CCS-5), 1998, pages 112-121.
• J.C. Mitchell, M. Mitchell, and A. Scedrov, A linguistic characterization of bounded oracle computation and probabilistic polynomial time, IEEE Foundations of Computer Science, 1998, pages 725-733.

Multiset rewriting, related logical methods, decision procedures, and lower bounds

• I. Cervesato, N.D. Durgin, P.D. Lincoln, J.C. Mitchell, and A. Scedrov, Journal of Computer Security, volume 13, issue 2, 2005, pages 265-316.
• R. Chadha, J.C. Mitchell, A. Scedrov, and V. Shmatikov, Contract signing, optimism, and advantage, CONCUR 2003, Marseille, France, Springer LNCS Volume 2761, Springer-Verlag, 2003, pp. 366-382.
• Durgin, N.A., Lincoln, P.D., Mitchell, J.C., and Scedrov, A., Multiset rewriting and the complexity of bounded security protocols, Journal of Computer Security, vol 12, number 1, 2004, pages 677-722.
• I. Cervesato, N.A. Durgin, J.C. Mitchell, P.D. Lincoln, and A. Scedrov, A Comparison between Strand Spaces and Multiset Rewriting for Security Protocol Analysis, International Symposium on Software Security, In M. Okada, B. Pierce, A. Scedrov, H. Tokuda, and A. Yonezawa, eds., Software Security - Theories and Systems. Mext-NSF-JSPS International Symposium, ISSS 2002, Tokyo, Japan, November 8-10, 2002. Springer LNCS Volume 2609, Springer-Verlag, 2003, pp. 356 - 383.
• H. Comon, V. Cortier, and J.C. Mitchell, Tree Automata with one Memory, Set Constraints and Ping-Pong Protocols, ICALP 2001, Crete, Greece, July 8-12, 2001.
• I. Cervesato, N.A. Durgin, J.C. Mitchell, P.D. Lincoln, and A. Scedrov, Relating strands and multiset rewriting for security protocol analysis, 13-th IEEE Computer Security Foundations Workshop, Cambridge, U.K., July 3-5, 2000, pages 35-51.
• N.A. Durgin, P.D. Lincoln, J.C. Mitchell, and A. Scedrov, Undecidability of bounded security protocols, Workshop on Formal Methods and Security Protocols (FMSP'99), Trento, Italy, July 5, 1999. Electronic proceedings
• I. Cervesato, N.A. Durgin, P.D. Lincoln, J.C. Mitchell, and A. Scedrov, A meta-notation for protocol analysis, 12-th IEEE Computer Security Foundations Workshop, Mordano, Italy, June 28-30, 1999.
• N.A. Durgin, and J.C. Mitchell, Analysis of Security Protocols. In Calculational System Design, ed. M. Broy and R. Steinbruggen, IOS Press, 1999, pages 369-395.

Malware Detection and Mitigation

• E. Stinson and J.C. Mitchell, Characterizing Bots' Remote Control Behavior, 4th GI Int'l Conf. on Detection of Intrusions & Malware, and Vulnerability Assessment (DIMVA), Lucerne, Switzerland, July, 2007.

Mobile Code Security

Java, RMI, and Jini Security

• N. Li and J.C. Mitchell, Securing Java RMI-based Distributed Applications, 20th Annual Computer Security Applications Conference (ACSAC 2004), Tucson, December, 2004.
• A. Chander, J.C. Mitchell, and I. Shin, Mobile code security by Java bytecode instrumentation, DARPA Information Survivability Conference & Exposition (DISCEX II), June, 2001.
• I. Shin and J.C. Mitchell, Java Bytecode Modification and Applet Security. Stanford CS Tech Report.

Java Bytecode Verifier

• S.N. Freund and J.C. Mitchell, A Type System for the Java Bytecode Language and Verifier, Journal of Automated Reasoning, volume 30 (3-4):271--321, 2003.
• S.N. Freund and J.C. Mitchell, A Formal Framework for the Java Bytecode Language and Verifier, ACM Conference on Object-Oriented Programming: Systems, Languages and Applications, Denver, CO, November, 1999, pages 147-166.
• S.N. Freund and J.C. Mitchell, A Type System for Object Initialization in the Java Bytecode Language, ACM Trans. Programming Languages and Systems, 21, 6 (Nov. 1999), pages 1196-1250.
• S.N. Freund and J.C. Mitchell, A Type System for Object Initialization in the Java Bytecode Language, ACM Symp. Object-oriented Programming: Systems, Languages and Applications (OOPSLA), 1998, pages 310-328.

Tamper-Resistant Code

• D. Lie, J. Mitchell, C. Thekkath, M. Horowitz, Specifying and Verifying Hardware for Tamper-Resistant Software, IEEE Symp. on Security and Privacy, Oakland, May 2003. (Bibtex, Paper)
• D. Lie, C. Thekkath, P. Lincoln, M. Mitchell, D. Boneh, J. Mitchell, M. Horowitz, Architectural Support for Copy and Tamper Resistant Software, Ninth International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS-IX), Cambridge, MA, November 12-15, 2000.  (Bibtex, Paper)
• D. Boneh, D. Lie, P.D. Lincoln, J.C. Mitchell, M. Mitchell, Hardware Support for Tamper-Resistant and Copy-Resistant Software, Technical Report CS-TN-00-97, Stanford University Computer Science, 2000.

Object Systems, Java design and Foundations

• Bono, V., Patel, A., Shmatikov, V., and Mitchell, J.C., A core calculus of classes and mixins, European Conference on Object-Oriented Programming, 1999, pages 43-66.
• Bono, V., Patel, A., Shmatikov, V., and Mitchell, J.C., A core language of classes and objects, 15th Conf. Mathematical Foundations of Programming Semantics, 1999.Proceedings appear as Volume 20, Electronic Notes in Theoretical Computer Science, 2000.
• Agesen, O., Freund, S., and Mitchell, J.C., Adding Type Parameterization to the Java Language, ACM Symp. Object-Oriented Programming: Systems, Languages and Applications (OOPSLA), 1997, pages 49-65.
• Fisher, K., and Mitchell, J.C., On the relationship between classes, objects and data abstraction, Theory and Practice of Object Systems 4,1 (1998) 3-32.
• Fisher, K., and Mitchell, J.C., The Development of Type Systems for Object-Oriented Languages, Theory and Practice of Object Systems 1,3 (1996) 189-220. (Bibtex)
• Fisher, K. and Mitchell, J.C., A delegation-based object calculus with subtyping, Proc. 10th Int'l Conf. Fundamentals of Computation Theory (FCT'95), Dresden, Germany, Springer LNCS 965, 1995, pages 42--61. (Invited paper.) (Bibtex)
• Fisher, K., Honsell, F. and Mitchell, J.C., A lambda calculus of objects and method specialization, Nordic J. Computing 1, 1 (1994) 3-37. (Bibtex)
• Katiyar, D., Luckham, D., and Mitchell, J.C., A type system for prototyping languages, Proc. 21st ACM Symp. on Principles of Programming Languages, 1994, pages 138--150. (Bibtex, Paper)
• Mitchell, J.C., Toward a typed foundation for method specialization and inheritance, Proc. 17th ACM Principles of Programming Languages Conf., January, 1990, pages 109--124. (Bibtex, Paper)
• Jategaonkar, L. and Mitchell, J.C., Type inference with extended pattern matching and subtypes, Fund. Informaticae 19 (1993) 127--166. (Bibtex, Paper)
• Cardelli, L. and Mitchell, J.C., Operations on records, Mathematical Structures in Computer Science 1 (1991) 3--48. (Bibtex, Short Summary, Paper)
• Canning, Cook, Hill, Mitchell and Olthoff, F-Bounded quantification for object-oriented programming, Proc. ACM Conf. Functional Programming and Computer Architecture, 1989, pages 273--280. (Bibtex, Paper)
• Mitchell, J.C., Type inference with simple subtypes, J. Functional Programming 1, 3 (1991) 245--286. (Bibtex, Paper)

Linear Logic

• Lincoln, P.D., Mitchell, J.C. and Scedrov, A., Optimization complexity of linear-logic proof games, Theor. Computer Science (to appear). Special issue on linear logic. (Bibtex, Paper)
• Lincoln, P.D., Mitchell, J.C. and Scedrov, A., The Complexity of Local Proof Search in Linear Logic (Extended Abstract), Proc. Linear Logic '96, Tokyo Meeting, Electronic Notes in Theoretical Computer Science, Volume 3 (1996) 10 pp., to appear. Preliminary report in CADE-13 Workshop on Proof Search in Type-Theoretic Languages, New Brunswick, NJ, July, 1996. (Bibtex, ENTCS site)
  Available here until ENTCS link to paper is operational.
• Lincoln, P.D., J.C. Mitchell and A. Scedrov, Stochastic interaction and linear logic. In Advances in Linear Logic, ed. J.-Y Girard, Y. Lafont and L. Regnier, London Mathematical Society Lecture Notes, Volume 222, Cambridge University Press, 1995, pages 147--166. (Bibtex, Paper)
• Lincoln, P.D., Mitchell, J.C. and Scedrov, A., Linear Logic Proof Games and Optimization, Research announcement accepted for publication in Bulletin of Symbolic Logic, 15 pp., 1996. (Bibtex, BSL site)
  Available here until BSL link to paper is operational.
• Lincoln, P., Mitchell, J.C., Scedrov, A. and Shankar, N., Decision Problems for Propositional Linear Logic, Ann. Pure and Applied Logic 56 (1992) 239--311. (Bibtex, Paper)

Type Theory and Semantics

• R. Harper and J.C. Mitchell, Parametricity and variants of Girard's J operator, Information Processing Letters 70, 1999, pages 1-5.
• Mitchell, J.C. and Viswanathan, R., Effective models of polymorphism, subtyping and recursion, 23rd International Colloquium on Automata, Languages, and Programming, (ICALP '96), Springer LNCS 1099, 1996, pages 170-181. (Bibtex, Paper)
• Hoang, M. and Mitchell, J.C., Lower bounds on type inference with subtypes, Proc. 22nd ACM Symp. on Principles of Programming Languages, 1995, pages 176-185. (Bibtex, Paper)
• Mitchell, J. and Viswanathan, R., Standard ML-NJ weak polymorphism and imperative constructs, Information and Computation, accepted for publication. (Special issue of papers from IEEE Symp. Logic in Computer Science, 1993.) (Bibtex, Paper)
• Harper, R. and Mitchell, J.C., The type structure of Standard ML, ACM Trans. Programming Languages and Systems, 15, 2 (1993) 211--252. (Bibtex, Paper)
• Bruce, K. and Mitchell, J.C., PER models of subtyping, recursive types and higher-order polymorphism, Proc. 19th ACM Principles of Programming Languages Conf., Albuquerque, January 19-22, 1992, pages 316-327.(Bibtex, Paper)
• Lincoln, P.D. and Mitchell, J.C., Algorithmic aspects of type inference with subtypes, Proc. 19th ACM Principles of Programming Languages Conf., Albuquerque, January 19-22, 1992, pages 293-304.(Bibtex, Paper)
• Kanellakis, P.C., Mairson, H.G. and Mitchell, J.C., Unification and ML type reconstruction. In Computational Logic: Essays in Honor of Alan Robinson, ed. J.-L. Lassez and G.D. Plotkin, MIT Press, 1991, pages 444-478. (Bibtex, Paper)
• Mitchell, J.C., On abstraction and the expressive power of programming languages. Science of Computer Programming 212 (1993) 141--163. (Special issue of papers from Symp. Theor. Aspects of Computer Software, Sendai, Japan, 1991.) (Bibtex, Paper)
• Mitchell, J.C., On the equivalence of data representations. In Artificial Intelligence and Mathematical Theory of Computation: Papers in Honor of John McCarthy, ed. V. Lifschitz, Academic Press, 1991, pages 305-330. (Bibtex, Paper)
• Harper, R., Mitchell, J.C. and Moggi, E., Higher-order modules and the phase distinction, Proc. 17th ACM Principles of Programming Languages Conf., San Francisco, January 17--19, 1990, pages 341-354.(Bibtex, Paper)
• J.C. Mitchell and G.D. Plotkin, Abstract types have existential type, ACM Trans. Programming Languages and Systems, 10, 3 (1988) 470--502. (Journal version of previous conference paper; Bibtex)
• Mitchell, J.C. and E. Moggi, Kripke-style Models for Typed Lambda Calculus, Proc. IEEE Symp. Logic in Computer Science, 1987, pages 303--314.

Other

• Mitchell, J.C., Hoang, M.K. and Howard, B., Labeling techniques and typed fixed-point operators, Workshop on Higher-order Operational Techniques, Cambridge, U.K. (Bibtex, Paper)
• Mitchell, J.C. and Scedrov, A., Notes on sconing and relators, Computer Science Logic '92, Selected Papers, E. Borger et al., eds., Springer LNCS 702, 1993, pages 352--378. (Bibtex, Paper)
• Dwork, C., Kanellakis, P.C. and Mitchell, J.C., On the sequential nature of unification, J. Logic Programming 1 (1984) 35--50. (Bibtex, Paper)
• Mitchell, J.C., The implication problem for functional and inclusion dependencies, Information and Control 56 (1983) 154-173. (Bibtex)