Selected Publications

Status: Links to bibtex entries and manuscripts should work. Links to abstracts are under construction.

Security and Electronic Commerce Protocols

Automated Analysis

• Shmatikov, V. and Mitchell, J.C., Analysis of Abuse-Free Contract Signing, Financial Cryptography ’00, accepted for publication.
• Shmatikov, V. and Mitchell, J.C., Analysis of a Fair Exchange Protocol, Seventh Annual Symposium on Network and Distributed System Security (NDSS 2000), accepted for publication.
• Mitchell, J.C., Shmatikov, V. and Stern, U., 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. (Abstract, Bibtex, Paper)
• Mitchell, J.C., Mitchell, M. and Stern, U., Automated Analysis of Cryptographic Protocols Using Murphi, IEEE Symp. Security and Privacy, Oakland, 1997, pages 141-153. (Abstract, Bibtex, Paper)

General methods and limitations

• Durgin, N.A., Lincoln, P.D., Mitchell, J.C., and Scedrov, A., Undecidability of bounded security protocols, Workshop on Formal Methods and Security Protocols (FMSP'99), Trento, Italy, July 5, 1999. Electronic proceedings:
• Cervesato,I., Durgin, N.A., Lincoln, P.D., Mitchell, J.C., and Scedrov, A., A meta-notation for protocol analysis, 12-th IEEE Computer Security Foundations Workshop, Mordano, Italy, June 28-30, 1999. (Abstract, Bibtex, Paper)
• Durgin, N.A. and Mitchell, J.C., Analysis of Security Protocols. In Calculational System Design, ed. M. Broy and R. Steinbruggen, IOS Press, 1999, pages 369--395. (Abstract, Bibtex, Paper)

Probabilistic Foundations

• 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. (Abstract, Bibtex, Paper)
• 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. (Abstract, Bibtex, Paper)
• Mitchell, J.C., Mitchell, M. and Scedrov, A., A linguistic characterization of bounded oracle computation and probabilistic polynomial time, IEEE Foundations of Computer Science, 1998, pages 725-733. (Abstract, Bibtex, Paper)

Mobile Code

Java Bytecode Verifier

• Freund, S.N., and Mitchell, J.C., 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.
• Freund, S.N. and Mitchell, J.C., A Type System for Object Initialization in the Java Bytecode Language, ACM Trans. Programming Languages and Systems (accepted for publication).
• Freund, S. and Mitchell, J.C., 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. (Abstract, Bibtex, Paper)

Java Applet Security

• Shin, I.. and Mitchell, J.C., Java Bytecode Modification and Applet Security. Unpublished (Stanford CS Tech Report). (Abstract, Bibtex, Paper)

Object Systems

• Bono, V., Patel, A., Shmatikov, V., and Mitchell, J.C., A core calculus of classes and mixins, European Conference on Object-Oriented Programming, 1999 (accepted for publication).
• 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.
• Agesen, O., Freund, S., and Mitchell, J.C., Adding Type Parameterization to the Java Language, ACM Symp. Object-Oriented Programming: Systems, Languages and Applications, 1997, pages 49-65. (Abstract, Bibtex, Paper)
• 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. (Abstract, Bibtex, Paper)
• 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. (Abstract, Bibtex, Paper)
• 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.) (Abstract, Bibtex, Paper)
• Fisher, K., Honsell, F. and Mitchell, J.C., A lambda calculus of objects and method specialization, Nordic J. Computing 1, 1 (1994) 3-37. (Abstract, 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. (Abstract, 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. (Abstract, Bibtex, Paper)
• 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. (Abstract, Bibtex, Paper)
• Jategaonkar, L. and Mitchell, J.C., Type inference with extended pattern matching and subtypes, Fund. Informaticae 19 (1993) 127--166. (Abstract, Bibtex, Paper)
• Cardelli, L. and Mitchell, J.C., Operations on records, Mathematical Structures in Computer Science 1 (1991) 3--48. (Abstract, Bibtex, Short Summary)
• 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. (Abstract, Bibtex, Paper)
• Mitchell, J.C., Type inference with simple subtypes, J. Functional Programming 1, 3 (1991) 245--286. (Abstract, 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. (Abstract, 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. (Abstract, 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. (Abstract, 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. (Abstract, 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. (Abstract, Bibtex, Paper)

Type Theory and Semantics

• 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. (Abstract, 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.) (Abstract, 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. (Abstract, 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.) (Abstract, 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. (Abstract, 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. (Abstract, Bibtex, Paper)
• Mitchell, J.C. and Plotkin, G.D., Abstract types have existential type, ACM Trans. Programming Languages and Systems, 10, 3 (1988) 470--502. (Abstract, Bibtex, Paper)

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. (Abstract, 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. (Abstract, Bibtex, Paper)
• Dwork, C., Kanellakis, P.C. and Mitchell, J.C., On the sequential nature of unification, J. Logic Programming 1 (1984) 35--50. (Abstract, Bibtex)
• Mitchell, J.C., The implication problem for functional and inclusion dependencies, Information and Control 56 (1983) 154--173. (Abstract, Bibtex)