John Mitchell

All Publications

• Remote Learning and Work IEEE INTERNET COMPUTING Kizilcec, R., Mitchell, J. 2024; 28 (1): 7-9

  View details for DOI 10.1109/MIC.2023.3339941

  View details for Web of Science ID 001166996500005

• Detecting the Reasons for Program Decomposition in CS1 and Evaluating Their Impact ACM Technical Symposium on Computer Science Education Charitsis, C., Piech, C., Mitchell, J. C. 2023: 2023

  View details for DOI 10.1145/3545945.3569763

• Insights for post-pandemic pedagogy across one CS department Bigman, M., Gilon, Y., Han, J., Mitchell, J. C. Arxiv. 2022

  Abstract

  Adaptive remote instruction has led to important lessons for the future, including rediscovery of known pedagogical principles in new contexts and new insights for supporting remote learning. Studying one computer science department that serves residential and remote undergraduate and graduate students, we conducted interviews with stakeholders in the department (n=26) and ran a department-wide student survey (n=102) during the four academic quarters from spring 2020 to spring 2021. Our case study outlines what the instructors did, summarizes what instructors and students say about courses during this period, and provides recommendations for CS departments with similar scope going forward. Specific insights address: (1) how instructional components are best structured for students; (2) how students are assessed for their learning; and (3) how students are supported in student-initiated components of learning. The institution is a large U.S. research university that has a history of online programs including online enrollment in regular on-campus courses and large-scale open enrollment courses. Our recommendations to instructors across the scope of this department may also be applicable to other institutions that provide technology-supported in-person instruction, remote enrollment, and hybrid courses combining both modalities.

• Using NLP to quantify program decomposition in CS1 ACM Conference on Learning @ Scale Charitsis, C., Piech, C., Mitchell, J. C. 2022: 113-120

  View details for DOI 10.1145/3491140.3528272

• Function Names: Quantifying the Relationship Between Identifiers and Their Functionality to Improve Them ACM Conference on Learning @ Scale Charitsis, C., Piech, C., Mitchell, J. C. 2022: 93-101

  View details for DOI 10.1145/3491140.3528269

• Feedback on Program Development Process for CS1 Students ACM Technical Symposium on Computer Science Education Charitsis, C., Piech, C., Mitchell, J. C. 2022: 1150

  View details for DOI 10.1145/3478432.3499062

• Assessing Function Names and Quantifying the Relationship Between Identifiers and Their Functionality to Improve Them Charitsis, C., Piech, C., Mitchell, J. C. 2021: 291-293

  View details for DOI 10.1145/3430895.3460161

• Simplifying Automated Assessment in CS1 International Conference on Education Technology Management Chartists, C., Piech, C., Mitchell, J. C. 2021: 226-231

  View details for DOI 10.1145/3510309.3510345

• Model Checking Bitcoin and other Proof-of-Work Consensus Protocols DiGiacomo-Castillo, M., Liang, ., Pal, A., Mitchell, J. C. 2020 IEEE International Conference on Blockchain. 2020
• Model Checking Bitcoin and other Proof-of-Work Consensus Protocols DiGiacomo-Castillo, M., Liang, Y., Pal, A., Mitchell, J. C., IEEE Comp Soc IEEE COMPUTER SOC. 2020: 351-358

  View details for DOI 10.1109/Blockchain50366.2020.00051

  View details for Web of Science ID 000647642100042

• Reinforcement Learning for the Adaptive Scheduling of Educational Activities Bassen, J., Balaji, B., Schaarschmidt, M., Thille, C., Painter, J., Zimmaro, D., Gamest, A., Fast, E., Mitchell, J. C., ACM ASSOC COMPUTING MACHINERY. 2020

  View details for DOI 10.1145/3313831.3376518

  View details for Web of Science ID 000695438100189

• Teaching Online in 2020: Experiments, Empathy, Discovery Bigman, M., Mitchell, J. C. IEEE Learning With MOOCS (LWMOOCS). 2020
• Reinforcement Learning for the Adaptive Scheduling of Educational Activities Bassen, J., Balaji, B., Schaarschmidt, M., Thille, C., Painter, J., Zimmaro, D., Games, A., Fast, E., Mitchell, J. C. Proc 2020 CHI Conference on Human Factors in Computing Systems. 2020
• Automated Analysis of Cryptographic Assumptions in Generic Group Models JOURNAL OF CRYPTOLOGY Barthe, G., Fagerholm, E., Fiore, D., Mitchell, J., Scedrov, A., Schmidt, B. 2019; 32 (2): 324–60

  View details for DOI 10.1007/s00145-018-9302-3

  View details for Web of Science ID 000462213500002

• Data Oblivious Genome Variants Search on Intel SGX Mandal, A., Mitchell, J. C., Montgomery, H., Roy, A., GarciaAlfaro, J., HerreraJoancomarti, J., Livraga, G., Rios, R. SPRINGER INTERNATIONAL PUBLISHING AG. 2018: 296–310

  View details for DOI 10.1007/978-3-030-00305-0_21

  View details for Web of Science ID 000477970100021

• Flexible dynamic information flow control in the presence of exceptions JOURNAL OF FUNCTIONAL PROGRAMMING Stefan, D., Mazieres, D., Mitchell, J. C., Russo, A. 2017; 27

  View details for DOI 10.1017/S0956796816000241

  View details for Web of Science ID 000393984200001

• Privacy for Targeted Advertising Mandal, A., Mitchell, J., Montgomery, H., Roy, A., IEEE IEEE. 2017: 438–43

  View details for Web of Science ID 000426981000067

• Hails: Protecting data privacy in untrusted web applications JOURNAL OF COMPUTER SECURITY Giffin, D., Levy, A., Stefan, D., Terei, D., Mazieres, D., Mitchell, J., Russo, A. 2017; 25 (4-5): 427–61

  View details for DOI 10.3233/JCS-15801

  View details for Web of Science ID 000405374600004

• Evaluating the privacy properties of telephone metadata PROCEEDINGS OF THE NATIONAL ACADEMY OF SCIENCES OF THE UNITED STATES OF AMERICA Mayer, J., Mutchler, P., Mitchell, J. C. 2016; 113 (20): 5536-5541

  Abstract

  Since 2013, a stream of disclosures has prompted reconsideration of surveillance law and policy. One of the most controversial principles, both in the United States and abroad, is that communications metadata receives substantially less protection than communications content. Several nations currently collect telephone metadata in bulk, including on their own citizens. In this paper, we attempt to shed light on the privacy properties of telephone metadata. Using a crowdsourcing methodology, we demonstrate that telephone metadata is densely interconnected, can trivially be reidentified, and can be used to draw sensitive inferences.

  View details for DOI 10.1073/pnas.1508081113

  View details for Web of Science ID 000375977600032

  View details for PubMedID 27185922

  View details for PubMedCentralID PMC4878528

• Target Fragmentation in Android Apps Mutchler, P., Safaei, Y., Doupe, A., Mitchell, J., IEEE IEEE. 2016: 204–13

  View details for DOI 10.1109/SPW.2016.31

  View details for Web of Science ID 000391256200026

• Fast Algorithms for Learning with Long N-grams via Suffix Tree Based Matrix Multiplication Paskov, H. S., Mitchell, J. C., Hastie, T. J., Meila, M., Heskes, T. AUAI PRESS. 2015: 672–81

  View details for Web of Science ID 000493121100069

• Automated Analysis of Cryptographic Assumptions in Generic Group Models Barthe, G., Fagerholm, E., Fiore, D., Mitchell, J., Scedrov, A., Schmidt, B., Garay, J. A., Gennaro, R. SPRINGER-VERLAG BERLIN. 2014: 95–112

  View details for Web of Science ID 000371334500006

• Principles of Security and Trust - Second International Conference, POST 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software edited by Basin, David, A., Mitchell, John, C. 2013
• Oblivious program execution and path-sensitive non-interference IEEE 26th Computer Security Foundations Symposium Planul, J., Mitchell, J. C. IEEE. 2013: 66–80

  View details for DOI 10.1109/CSF.2013.12

  View details for Web of Science ID 000335225600005

• Oblivious Program Execution and Path-Sensitive Non-interference. Planul, J., Mitchell, John, C. 2013
• Compressive Feature Learning. Paskov, Hristo, S., West, R., Mitchell, John, C., Hastie, Trevor, J. 2013
• Addressing Covert Termination and Timing Channels in Concurrent Information Flow Systems ACM SIGPLAN NOTICES Stefan, D., Russo, A., Buiras, P., Levy, A., Mitchell, J. C., Mazieres, D. 2012; 47 (9): 201-213

  View details for DOI 10.1145/2398856.2364557

  View details for Web of Science ID 000311296000020

• A Learning-Based Approach to Reactive Security IEEE TRANSACTIONS ON DEPENDABLE AND SECURE COMPUTING Barth, A., Rubinstein, B. I., Sundararajan, M., Mitchell, J. C., Song, D., Bartlett, P. L. 2012; 9 (4): 482-493

  View details for DOI 10.1109/2011.42

  View details for Web of Science ID 000304147900005

• Privacy and Cybersecurity: The Next 100 Years PROCEEDINGS OF THE IEEE Landwehr, C., Boneh, D., Mitchell, J. C., Bellovin, S. M., Landau, S., Lesk, M. E. 2012; 100: 1659-1673

  View details for DOI 10.1109/JPROC.2012.2189794

  View details for Web of Science ID 000309838000049

• Information-flow control for programming on encrypted data 25th IEEE Computer Security Foundations Symposium (CSF) Mitchell, J. C., Sharma, R., Stefan, D., Zimmerman, J. IEEE. 2012: 45–60

  View details for DOI 10.1109/CSF.2012.30

  View details for Web of Science ID 000309007800004

• Disjunction Category Labels 16th Nordic Conference on Secure IT-Systems (NordSec) Stefan, D., Russo, A., Mazieres, D., Mitchell, J. C. SPRINGER-VERLAG BERLIN. 2012: 223–239

  View details for Web of Science ID 000310342000016

• SessionJuggler: secure web login from an untrusted terminal using session hijacking. Bursztein, E., Soman, C., Boneh, D., Mitchell, John, C. 2012
• Addressing covert termination and timing channels in concurrent information flow systems. Stefan, D., Russo, A., Buiras, P., Levy, A., Mitchell, John, C., Mazières, D. 2012
• Declarative privacy policy: finite models and attribute-based encryption. Lam, Peifung, E., Mitchell, John, C., Scedrov, A., Sundaram, S., Wang, F. 2012
• Information-Flow Control for Programming on Encrypted Data. Mitchell, John, C., Sharma, R., Stefan, D., Zimmerman, J. 2012
• Information-flow control for programming on encrypted data. IACR Cryptology ePrint Archive Mitchell, John, C., Sharma, R., Stefan, D., Zimmerman, J. 2012: 205
• Flexible Dynamic Information Flow Control in the Presence of Exceptions. CoRR abs/1207.1457 Stefan, D., Russo, A., Mitchell, John, C., Mazières, D. 2012
• Third-Party Web Tracking: Policy and Technology. Mayer, Jonathan, R., Mitchell, John, C. 2012
• Third-Party Web Tracking: Policy and Technology 33rd IEEE Symposium on Security and Privacy (SP) Mayer, J. R., Mitchell, J. C. IEEE. 2012: 413–427

  View details for DOI 10.1109/SP.2012.47

  View details for Web of Science ID 000309219900027

• Flexible Dynamic Information Flow Control in Haskell ACM SIGPLAN NOTICES Stefan, D., Russo, A., Mitchell, J. C., Mazieres, D. 2011; 46 (12): 95-106

  View details for DOI 10.1145/2096148.2034688

  View details for Web of Science ID 000299326600009

• A 1-year follow-up of a multi-center treatment trial of adults with anorexia nervosa EATING AND WEIGHT DISORDERS-STUDIES ON ANOREXIA BULIMIA AND OBESITY Yu, J., Agras, W. S., HALMI, K. A., Crow, S., Mitchell, J., Bryson, S. W. 2011; 16 (3): E177-E181

  Abstract

  To examine maintenance of recovery following treatment in an adult anorexia nervosa (AN) population.One year follow-up of a randomized clinical trial with 122 participants treated with: cognitive behavioral therapy (CBT), drug therapy (fluoxetine), or a combination (CBT+fluoxetine) for 12 months. Participants were assessed at baseline, end of treatment, and follow-up. The primary outcomes were weight and the global scores from the Eating Disorder Examination (EDE) separately and combined.Fifty-two participants completed the follow-up. Mean weight increased from end of treatment to follow-up. Seventy-five percent (75%) of those weight recovered at end of treatment maintained this recovery at follow-up. Recovery of eating disorder psychopathology was stable from end of treatment to follow-up, with 40% of participants with a global EDE score within normal range. Using the most stringent criteria for recovery, only 21% of the completer sample was recovered.The findings suggest that while adults with AN improve with treatment and maintain these improvements during follow-up, the majority is not recovered. Additionally, further research is needed to understand barriers to treatment and assessment completion.

  View details for Web of Science ID 000303170600005

  View details for PubMedID 22290033

• Security Modeling and Analysis IEEE SECURITY & PRIVACY Bau, J., Mitchell, J. C. 2011; 9 (3): 18-25

  View details for DOI 10.1109/MSP.2011.2

  View details for Web of Science ID 000290999800004

• A Symbolic Logic with Exact Bounds for Cryptographic Protocols. Mitchell, John, C. 2011
• Flexible Dynamic Information Flow Control in Haskell Stefan, D., Russo, A., Mitchell, J. C., Mazieres, D., ACM ASSOC COMPUTING MACHINERY. 2011: 95–106

  View details for Web of Science ID 000304130300009

• Program Analysis for Web Security Mitchell, J. C., Yahav, E. SPRINGER-VERLAG BERLIN. 2011: 4

  View details for Web of Science ID 000306978900003

• Text-based CAPTCHA Strengths and Weaknesses Bursztein, E., Martin, M., Mitchell, J. C., ACM ASSOC COMPUTING MACHINERY. 2011: 125–37

  View details for Web of Science ID 000397423700012

• A Domain-Specific Language for Computing on Encrypted Data Bain, A., Mitchell, J., Sharma, R., Stefan, D., Zimmerman, J., Chakraborty, S., Kumar, A. SCHLOSS DAGSTUHL, LEIBNIZ CENTER INFORMATICS. 2011: 6–24

  View details for DOI 10.4230/LIPIcs.FSTTCS.2011.6

  View details for Web of Science ID 000392597900004

• The Failure of Noise-Based Non-Continuous Audio Captchas 32nd IEEE Symposium on Security and Privacy (SP 2011) Bursztein, E., Beauxis, R., Paskov, H., Perito, D., Fabry, C., Mitchell, J. IEEE COMPUTER SOC. 2011: 19–31

  View details for DOI 10.1109/SP.2011.14

  View details for Web of Science ID 000295408400002

• Reclaiming the Blogosphere, TalkBack: A Secure LinkBack Protocol for Weblogs 16th European Symposium on Research in Computer Security (ESORICS 2011) Bursztein, E., Gourdin, B., Mitchell, J. C. SPRINGER-VERLAG BERLIN. 2011: 133–149

  View details for Web of Science ID 000307366400008

• A Symbolic Logic with Exact Bounds for Cryptographic Protocols 18th Workshop on Logic, Language, Information and Computation (WoLLIC) Mitchell, J. C. SPRINGER-VERLAG BERLIN. 2011: 3–3

  View details for Web of Science ID 000312033400003

• Automated Analysis of Security-Critical JavaScript APIs 32nd IEEE Symposium on Security and Privacy (SP 2011) Taly, A., Erlingsson, U., Mitchell, J. C., Miller, M. S., Nagra, J. IEEE COMPUTER SOC. 2011: 363–378

  View details for DOI 10.1109/SP.2011.39

  View details for Web of Science ID 000295408400023

• Automated Analysis of Security-Critical JavaScript APIs. Taly, A., Erlingsson, Ú., Mitchell, John, C., Miller, Mark, S., Nagra, J. 2011
• The Failure of Noise-Based Non-continuous Audio Captchas. Bursztein, E., Beauxis, R., Paskov, Hristo, S., Perito, D., Fabry, C., Mitchell, John, C. 2011
• Program Analysis for Web Security. Mitchell, John, C. 2011
• Disjunction Category Labels. Stefan, D., Russo, A., Mazières, D., Mitchell, John, C. 2011
• Reclaiming the Blogosphere, TalkBack: A Secure LinkBack Protocol for Weblogs. Bursztein, E., Gourdin, B., Mitchell, John, C. 2011
• Text-based CAPTCHA strengths and weaknesses. Bursztein, E., Martin, M., Mitchell, John, C. 2011
• TBA : A Hybrid of Logic and Extensional Access Control Systems. Formal Aspects in Security and Trust Hinrichs, Timothy, L., Garrison III, William, C., Lee, Adam, J., Saunders, S., Mitchell, John, C. 2011
• A Domain-Specific Language for Computing on Encrypted Data. IACR Cryptology ePrint Archive Bain, A., Mitchell, John, C., Sharma, R., Stefan, D., Zimmerman, J. 2011: 561
• Inductive trace properties for computational security. Journal of Computer Security Roy, A., Datta, A., Derek, A., Mitchell, John, C. 2010; 6 (18): 1035-1073
• Inductive trace properties for computational security JOURNAL OF COMPUTER SECURITY Roy, A., Datta, A., Derek, A., Mitchell, J. 2010; 18 (6): 1035–73

  View details for DOI 10.3233/JCS-2009-389

  View details for Web of Science ID 000210967900004

• Using Strategy Objectives for Network Security Analysis 5th China International Conference on Information Security and Cryptology Bursztein, E., Mitchell, J. C. SPRINGER-VERLAG BERLIN. 2010: 337–349

  View details for Web of Science ID 000286442600025

• State of the Art: Automated Black-Box Web Application Vulnerability Testing Symposium on Security and Privacy Bau, J., Bursztein, E., Gupta, D., Mitchell, J. IEEE COMPUTER SOC. 2010: 332–345

  View details for DOI 10.1109/SP.2010.27

  View details for Web of Science ID 000287456100023

• Towards a Formal Foundation of Web Security 23rd IEEE Computer Security Foundations Symposium (CSF)/Federated Logic Conference Akhawe, D., Barth, A., Lam, P. E., Mitchell, J., Song, D. IEEE COMPUTER SOC. 2010: 290–304

  View details for DOI 10.1109/CSF.2010.27

  View details for Web of Science ID 000308460400020

• Object Capabilities and Isolation of Untrusted Web Applications Symposium on Security and Privacy Maffeis, S., Mitchell, J. C., Taly, A. IEEE COMPUTER SOC. 2010: 125–140

  View details for DOI 10.1109/SP.2010.16

  View details for Web of Science ID 000287456100010

• How Good are Humans at Solving CAPTCHAs? A Large Scale Evaluation Symposium on Security and Privacy Bursztein, E., Bethard, S., Fabry, C., Mitchell, J. C., Jurafsky, D. IEEE COMPUTER SOC. 2010: 399–413

  View details for DOI 10.1109/SP.2010.31

  View details for Web of Science ID 000287456100027

• A Security Evaluation of DNSSEC with NSEC3. IACR Cryptology ePrint Archive Bau, J., Mitchell, John, C. 2010: 115
• A Learning-Based Approach to Reactive Security. Financial Cryptography Barth, A., Rubinstein, Benjamin, I. P., Sundararajan, M., Mitchell, John, C. 2010
• A Security Evaluation of DNSSEC with NSEC3. Bau, J., Mitchell, John, C. 2010
• How Good Are Humans at Solving CAPTCHAs? A Large Scale Evaluation. Bursztein, E., Bethard, S., Fabry, C., Mitchell, John, C., Jurafsky, D. 2010
• State of the Art: Automated Black-Box Web Application Vulnerability Testing. Bau, J., Bursztein, E., Gupta, D., Mitchell, John, C. 2010
• Object Capabilities and Isolation of Untrusted Web Applications. Maffeis, S., Mitchell, John, C., Taly, A. 2010
• Towards a Formal Foundation of Web Security. Akhawe, D., Barth, A., Lam, Peifung, E., Mitchell, John, C., Song, D. 2010
• A Learning-Based Approach to Reactive Security 14th Financial Cryptography and Data Security International Conference Barth, A., Rubinstein, B. I., Sundararajan, M., Mitchell, J. C., Song, D., Bartlett, P. L. SPRINGER-VERLAG BERLIN. 2010: 192–206

  View details for Web of Science ID 000286416700016

• A 4-Year Prospective Study of Eating Disorder NOS Compared with Full Eating Disorder Syndromes INTERNATIONAL JOURNAL OF EATING DISORDERS Agras, W. S., Crow, S., Mitchell, J. E., Halmi, K. A., Bryson, S. 2009; 42 (6): 565-570

  Abstract

  To examine the course of Eating Disorder NOS (EDNOS) compared with anorexia nervosa (AN), bulimia nervosa (BN), and binge eating disorder (BED).Prospective study of 385 participants meeting DSM-IV criteria for AN, BN, BED, and EDNOS at three sites. Recruitment was from the community and specialty clinics. Participants were followed at 6-month intervals during a 4-year period using the Eating Disorder Examination as the primary assessment.EDNOS remitted significantly more quickly that AN or BN but not BED. There were no differences between EDNOS and full ED syndromes, or the subtypes of EDNOS, in time to relapse following first remission. Only 18% of the EDNOS group had never had or did not develop another ED diagnosis during the study; however, this group did not differ from the remaining EDNOS group.EDNOS appears to be a way station between full ED syndromes and recovery, and to a lesser extent from recovery or EDNOS status to a full ED. Implications for DSM-V are examined.

  View details for DOI 10.1002/eat.20708

  View details for Web of Science ID 000269224000012

  View details for PubMedID 19544557

  View details for PubMedCentralID PMC2862563

• Securing Frame Communication in Browsers COMMUNICATIONS OF THE ACM Barth, A., Jackson, C., Mitchell, J. C. 2009; 52 (6): 83-91

  View details for DOI 10.1145/1516046.1516066

  View details for Web of Science ID 000266235300026

• An Automated Approach for Proving PCL Invariants ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE Mitchell, J. C., Roy, A., Sundararajan, M. 2009; 234: 93–113

  View details for DOI 10.1016/j.entcs.2009.02.074

  View details for Web of Science ID 000216906700007

• Isolating JavaScript with Filters, Rewriting, and Wrappers. Maffeis, S., Mitchell, John, C., Taly, A. 2009
• Isolating JavaScript with Filters, Rewriting, and Wrappers COMPUTER SECURITY - ESORICS 2009, PROCEEDINGS Maffeis, S., Mitchell, J. C., Taly, A. 2009; 5789: 505-?

  View details for Web of Science ID 000274011000031

• A Formalization of HIPAA for a Medical Messaging System. Lam, Peifung, E., Mitchell, John, C., Sundaram, S. 2009
• A Learning-Based Approach to Reactive Security. CoRR abs/0912.1155 Barth, A., Rubinstein, Benjamin, I. P., Sundararajan, M., Mitchell, John, C., Song, D. X., Bartlett, Peter, L. 2009
• Practical declarative network management. Hinrichs, Timothy, L., Gude, N., Casado, M., Mitchell, John, C., Shenker, S. 2009
• TrackBack spam: abuse and prevention. Bursztein, E., Lam, Peifung, E., Mitchell, John, C. 2009
• An Automated Approach for Proving PCL Invariants. Electr. Notes Theor. Comput. Sci. Mitchell, John, C., Roy, A., Sundararajan, M. 2009; 234: 93-113
• Using Strategy Objectives for Network Security Analysis. Bursztein, E., Mitchell, John, C. 2009
• On the relationships between notions of simulation-based security JOURNAL OF CRYPTOLOGY Kuesters, R., Datta, A., Mitchell, J. C., Ramanathan, A. 2008; 21 (4): 492-546

  View details for DOI 10.1007/s00145-008-9019-9

  View details for Web of Science ID 000258960700002

• A Layered Architecture for Detecting Malicious Behaviors. Martignoni, L., Stinson, E., Fredrikson, M., Jha, S., Mitchell, John, C. 2008
• A Layered Architecture for Detecting Malicious Behaviors RECENT ADVANCES IN INTRUSION DETECTION, RAID 2008 Martignoni, L., Stinson, E., Fredrikson, M., Jha, S., Mitchell, J. C. 2008; 5230: 78-?

  View details for Web of Science ID 000260067900005

• An Operational Semantics for JavaScript PROGRAMMING LANGUAGES AND SYSTEMS, PROCEEDINGS Maffeis, S., Mitchell, J. C., Taly, A. 2008; 5356: 307-?

  View details for Web of Science ID 000262126200022

• Analysis of EAP-GPSK Authentication Protocol. Mitchell, John, C., Roy, A., Rowe, P., Scedrov, A. 2008
• Securing Frame Communication in Browsers. Barth, A., Jackson, C., Mitchell, John, C. 2008
• An Operational Semantics for JavaScript. Maffeis, S., Mitchell, John, C., Taly, A. 2008
• Robust defenses for cross-site request forgery. Barth, A., Jackson, C., Mitchell, John, C. 2008
• Characterizing Bots' Remote Control Behavior. Botnet Detection Stinson, E., Mitchell, John, C. 2008: 45-64
• Towards Systematic Evaluation of the Evadability of Bot/Botnet Detection Methods. Stinson, E., Mitchell, John, C. 2008
• Protocol Composition Logic (PCL) ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE Datta, A., Derek, A., Mitchell, J. C., Roy, A. 2007; 172: 311–58

  View details for DOI 10.1016/j.entcs.2007.02.012

  View details for Web of Science ID 000214226000012

• Characterizing Bots' Remote Control Behavior. Stinson, E., Mitchell, John, C. 2007
• Protocol Composition Logic (PCL). Electr. Notes Theor. Comput. Sci. Datta, A., Derek, A., Mitchell, John, C., Roy, A. 2007; 172: 311-358
• Inductive Proof Method for Computational Secrecy. IACR Cryptology ePrint Archive Roy, A., Datta, A., Derek, A., Mitchell, John, C. 2007: 165
• Privacy and Utility in Business Processes. Barth, A., Mitchell, John, C., Datta, A., Sundaram, S. 2007
• Formal Proofs of Cryptographic Security of Diffie-Hellman-Based Protocols. Roy, A., Datta, A., Mitchell, John, C. 2007
• Inductive Proofs of Computational Secrecy. Roy, A., Datta, A., Derek, A., Mitchell, John, C. 2007
• Compositional analysis of contract-signing protocols 2nd Workshop on Automated Reasoning for Security Protocol Analysis Backes, M., Datta, A., Derek, A., Mitchell, J. C., Turuani, M. ELSEVIER SCIENCE BV. 2006: 33–56

  View details for DOI 10.1016/j.tcs.2006.08.039

  View details for Web of Science ID 000242424300003

• A probabilistic polynomial-time process calculus for the analysis of cryptographic protocols THEORETICAL COMPUTER SCIENCE Mitchell, J. C., Ramanathan, A., Scedrov, A., Teague, V. 2006; 353 (1-3): 118-164

  View details for DOI 10.1016/j.tcs.2005.10.044

  View details for Web of Science ID 000236230100007

• Games and the Impossibility of Realizable Ideal Functionality. Datta, A., Derek, A., Mitchell, John, C., Ramanathan, A., Scedrov, A. 2006
• Secrecy Analysis in Protocol Composition Logic. Roy, A., Datta, A., Derek, A., Mitchell, John, C., Seifert, J. 2006
• Protecting browser state from web privacy attacks. Jackson, C., Bortz, r., Boneh, D., Mitchell, John, C. 2006
• Computationally Sound Compositional Logic for Key Exchange Protocols. Datta, A., Derek, A., Mitchell, John, C., Warinschi, B. 2006
• Inductive Trace Properties for Computational Security. IACR Cryptology ePrint Archive Roy, A., Datta, A., Derek, A., Mitchell, John, C. 2006: 486
• On the Relationships Between Notions of Simulation-Based Security. IACR Cryptology ePrint Archive Datta, A., Küsters, R., Mitchell, John, C., Ramanathan, A. 2006: 153
• Understanding SPKI/SDSI using first-order logic. Int. J. Inf. Sec. Li, N., Mitchell, John, C. 2006; 1 (5): 48-64
• Managing Digital Rights using Linear Logic. Barth, A., Mitchell, John, C. 2006
• Privacy and Contextual Integrity: Framework and Applications. Barth, A., Datta, A., Mitchell, John, C., Nissenbaum, H. 2006
• Key Exchange Protocols: Security Definition, Proof Method and Applications. IACR Cryptology ePrint Archive Datta, A., Derek, A., Mitchell, John, C., Warinschi, B. 2006: 56
• Contract signing, optimism, and advantage JOURNAL OF LOGIC AND ALGEBRAIC PROGRAMMING CHADHA, R., Mitchell, J. C., Scedrov, A., Shmatikov, V. 2005; 64 (2): 189-218

  View details for DOI 10.1016/j.jlap.2004.09.003

  View details for Web of Science ID 000230226800003

• Beyond proof-of-compliance: Security analysis in trust management JOURNAL OF THE ACM Li, N. H., Mitchell, J. C., Winsborough, W. H. 2005; 52 (3): 474-514

  View details for Web of Science ID 000229985100003

• Probabilistic polynomial-time semantics for a protocol security logic 32nd International Colloquium on Automata, Languages and Programming (ICALP 2005) Datta, A., Derek, A., Mitchell, J. C., Shmatikov, V., Turuani, M. SPRINGER-VERLAG BERLIN. 2005: 16–29

  View details for Web of Science ID 000230880500002

• LEA derivation system and compositional logic for security protocols JOURNAL OF COMPUTER SECURITY Datta, A., Derek, A., Mitchell, J., Pavlovic, D. 2005; 13 (3): 423–82

  View details for Web of Science ID 000210788600004

• A comparison between strand spaces and multiset rewriting for security protocol analysis JOURNAL OF COMPUTER SECURITY Cervesato, I., Durgin, N. A., Lincoln, P. D., Mitchell, J. C., Scedrov, A. 2005; 13 (2): 265–316

  View details for DOI 10.3233/JCS-2005-13203

  View details for Web of Science ID 000210785100003

• Probabilistic Polynomial-Time Semantics for a Protocol Security Logic. Datta, A., Derek, A., Mitchell, John, C., Shmatikov, V., Turuani, M. 2005
• A modular correctness proof of IEEE 802.11i and TLS. He, C., Sundararajan, M., Datta, A., Derek, A., Mitchell, John, C. 2005
• A derivation system and compositional logic for security protocols. Journal of Computer Security Datta, A., Derek, A., Mitchell, John, C., Pavlovic, D. 2005; 3 (13): 423-482
• Compositional Analysis of Contract Signing Protocols. Backes, M., Datta, A., Derek, A., Mitchell, John, C., Turuani, M. 2005
• Security analysis of network protocols: logical and computational methods. Mitchell, John, C. 2005
• Games and the Impossibility of Realizable Ideal Functionality. IACR Cryptology ePrint Archive Datta, A., Derek, A., Mitchell, John, C., Ramanathan, A., Scedrov, A. 2005: 211
• Security Analysis and Improvements for IEEE 802.11i. He, C., Mitchell, John, C. 2005
• On the Relationships Between Notions of Simulation-Based Security. Datta, A., Küsters, R., Mitchell, John, C., Ramanathan, A. 2005
• Enterprise privacy promises and enforcement. Barth, A., Mitchell, John, C. 2005
• Proceedings of the 2005 ACM workshop on Formal methods in security engineering edited by Atluri, V., Samarati, P., Küsters, R. 2005
• Multiset rewriting and the complexity of bounded security protocols. Journal of Computer Security Durgin, Nancy, A., Lincoln, P., Mitchell, John, C. 2004; 2 (12): 247-311
• Client-Side Defense Against Web-Based Identity Theft. Chou, N., Ledesma, R., Teraguchi, Y., Mitchell, John, C. 2004
• A Distributed High Assurance Reference Monitor. Chander, A., Dean, D., Mitchell, John, C. 2004
• Probabilistic Bisimulation and Equivalence for Security Analysis of Network Protocols. Ramanathan, A., Mitchell, John, C., Scedrov, A., Teague, V. 2004
• Reconstructing Trust Management. Journal of Computer Security Chander, A., Dean, D., Mitchell, John, C. 2004; 1 (12): 131-164
• Analysis of the 802.11i 4-way handshake. He, C., Mitchell, John, C. 2004
• Conflict and combination in privacy policy languages. Barth, A., Mitchell, John, C., Rosenstein, J. 2004
• Securing Java RMI-Based Distributed Applications. Li, N., Mitchell, John, C., Tong, D. 2004
• Abstraction and Refinement in Protocol Derivation. Datta, A., Derek, A., Mitchell, John, C., Pavlovic, D. 2004
• Development of investigational radiation modifiers JOURNAL OF THE NATIONAL CANCER INSTITUTE Colevas, A. D., Brown, J. M., Hahn, S., Mitchell, J., Camphausen, K., Coleman, C. N. 2003; 95 (9): 646-651

  View details for Web of Science ID 000182672800007

  View details for PubMedID 12734315

• A type system for the Java bytecode language and verifier JOURNAL OF AUTOMATED REASONING Freund, S. N., Mitchell, J. C. 2003; 30 (3-4): 271-321

  View details for Web of Science ID 000184587600003

• Distributed Credential Chain Discovery in Trust Management. Journal of Computer Security Li, N., Winsborough, William, H., Mitchell, John, C. 2003; 1 (11): 35-86
• A Derivation System for Security Protocols and its Logical Formalization. Datta, A., Derek, A., Mitchell, John, C., Pavlovic, D. 2003
• Understanding SPKI/SDSI Using First-Order Logic. Li, N., Mitchell, John, C. 2003
• Beyond Proof-of-Compliance: Safety and Availability Analysis in Trust Management. Li, N., Winsborough, William, H., Mitchell, John, C. 2003
• Concepts in programming languages. Mitchell, John, C. Cambridge University Press. 2003
• Security by typing. STTT Debbabi, M., Durgin, Nancy, A., Mejri, M., Mitchell, John, C. 2003; 4 (4): 472-495
• Contract Signing, Optimism, and Advantage. Chadha, R., Mitchell, John, C., Scedrov, A., Shmatikov, V. 2003
• Specifying and Verifying Hardware for Tamper-Resistant Software. Lie, D., Mitchell, John, C., Thekkath, Chandramohan, A., Horowitz, M. 2003
• Secure protocol composition. Datta, A., Derek, A., Mitchell, John, C., Pavlovic, D. 2003
• DATALOG with Constraints: A Foundation for Trust Management Languages. Li, N., Mitchell, John, C. 2003
• A Role-based Trust-management Framework. Li, N., Mitchell, John, C. 2003
• Composition of Cryptographic Protocols in a Probabilistic Polynomial-Time Process Calculus. Mateus, P., Mitchell, John, C., Scedrov, A. 2003
• Relating cryptography and formal methods: a panel. Backes, M., Meadows, C., Mitchell, John, C. 2003
• A Compositional Logic for Proving Security Properties of Protocols. Journal of Computer Security Durgin, Nancy, A., Mitchell, John, C., Pavlovic, D. 2003; 4 (11): 677-722
• Finite-state analysis of two contract signing protocols THEORETICAL COMPUTER SCIENCE Shmatikov, V., Mitchell, J. C. 2002; 283 (2): 419-450

  View details for Web of Science ID 000176538500006

• Autonomous Nodes and Distributed Mechanisms. Mitchell, John, C., Teague, V. 2002
• Multiset rewriting and security protocol analysis REWRITING TECHNIQUES AND APPLICATIONS Mitchell, J. C. 2002; 2378: 19-22

  View details for Web of Science ID 000180069300002

• Design of a Role-Based Trust-Management Framework. Li, N., Mitchell, John, C., Winsborough, William, H. 2002
• A Comparison between Strand Spaces and Multiset Rewriting for Security Protocol Analysis. Cervesato, I., Durgin, Nancy, A., Lincoln, P., Mitchell, John, C., Scedrov, A. 2002
• Multiset Rewriting and Security Protocol Analysis. Mitchell, John, C. 2002
• Programming language methods in computer security 28th ACM/SIGPLAN/SIGACT Symposium on Principles of Programming Languages (POPL 2001) Mitchell, J. C. ASSOC COMPUTING MACHINERY. 2001: 1–3

  View details for Web of Science ID 000167936800001

• A Probabilistic Polynomial-time Calculus For Analysis of Cryptographic Protocols (Preliminary Report). Electr. Notes Theor. Comput. Sci. Mitchell, John, C., Ramanathan, A., Scedrov, A., Teague, V. 2001; 45: 280-310
• Distributed credential chain discovery in trust management: extended abstract. Li, N., Winsborough, William, H., Mitchell, John, C. 2001
• Programming language methods in computer security. Mitchell, John, C. 2001
• Probabilistic Polynominal-Time Process Calculus and Security Protocol Analysis. Mitchell, John, C., Ramanathan, A., Scedrov, A., Teague, V. 2001
• Probabilistic Polynomial-Time Process Calculus and Security Protocol Analysis. Mitchell, John, C. 2001
• A State-Transition Model of Trust Management and Access Control. Chander, A., Mitchell, John, C., Dean, D. 2001
• A Compositional Logic for Protocol Correctness. Durgin, Nancy, A., Mitchell, John, C., Pavlovic, D. 2001
• Architectural support for copy and tamper resistant software 9th International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS_IX) Lie, D., Thekkath, C., Mitchell, M., Lincoln, P., Boneh, D., Mitchell, J., Horowitz, M. ASSOC COMPUTING MACHINERY. 2000: 168–77

  View details for Web of Science ID 000165257200017

• Analysis of Abuse-Free Contract Signing. Financial Cryptography Shmatikov, V., Mitchell, John, C. 2000
• Analysis of a Fair Exchange Protocol. Shmatikov, V., Mitchell, John, C. 2000
• Relating Strands and Multiset Rewriting for Security Protocol Analysis. Cervesato, I., Durgin, Nancy, A., Mitchell, John, C., Lincoln, P., Scedrov, A. 2000
• A type system for object initialization in the Java bytecode language ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS Freund, S. N., Mitchell, J. C. 1999; 21 (6): 1196-1250

  View details for Web of Science ID 000086672600003

• A formal framework for the Java bytecode language and verifier ACM SIGPLAN NOTICES Freund, S. N., Mitchell, J. C. 1999; 34 (10): 147-166

  View details for Web of Science ID 000083510800013

• Optimization complexity of linear logic proof games Linear Logic 96 Tokyo Meeting Lincoln, P. D., Mitchell, J. C., Scedrov, A. ELSEVIER SCIENCE BV. 1999: 299–331

  View details for Web of Science ID 000083073200012

• Parametricity and variants of Girard's J operator INFORMATION PROCESSING LETTERS Harper, R., Mitchell, J. C. 1999; 70 (1): 1-5

  View details for Web of Science ID 000080537800001

• Probabilistic Polynomial-Time Equivalence and Security Analysis. Lincoln, P., Mitchell, John, C., Mitchell, M., Scedrov, A. 1999
• A Meta-Notation for Protocol Analysis. Cervesato, I., Durgin, Nancy, A., Lincoln, P., Mitchell, John, C., Scedrov, A. 1999
• The type system for object initializatiion in the Jave bytecode language. ACM Trans. Program. Lang. Syst. Freund, Stephen, N., Mitchell, John, C. 1999; 6 (21): 1196-1250
• A Formal Framework for the Java Bytecode Language and Verifier. Freund, Stephen, N., Mitchell, John, C. 1999
• A Core Calculus of Classes and Objects. Electr. Notes Theor. Comput. Sci. Bono, V., Mitchell, John, C., Patel, A., Shmatikov, V. 1999; 20: 28-49
• A type system for object initialization in the Java (TM) bytecode language ACM SIGPLAN NOTICES Freund, S. N., Mitchell, J. C. 1998; 33 (10): 310-328

  View details for Web of Science ID 000076378100027

• On the relationship between classes, objects, and data abstraction 3rd Workshop on Foundations of Object-Oriented Languages Fisher, K., Mitchell, J. C. JOHN WILEY & SONS INC. 1998: 3–25

  View details for Web of Science ID 000074393400002

• A Probabilistic Poly-Time Framework for Protocol Analysis. Lincoln, P., Mitchell, John, C., Mitchell, M., Scedrov, A. 1998
• A Type System for Object Initialization in the Java Bytecode Language. Freund, Stephen, N., Mitchell, John, C. 1998
• Finite-State Analysis of Security Protocols. Mitchell, John, C. 1998
• A Linguistic Characterization of Bounded Oracle Computation and Probabilistic Polynomial Time. Mitchell, John, C., Mitchell, M., Scedrov, A. 1998
• Adding type parameterization to the Java(TM) language 1997 ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages and Applications (OOPSLA 97) Agesen, O., Freund, S. N., Mitchell, J. C. ASSOC COMPUTING MACHINERY. 1997: 49–65

  View details for Web of Science ID A1997YE49200006

• ML and beyond Programming Languages Workshop of the Strategic Directions in Computing Research Harper, R., Mitchell, J. C. ASSOC COMPUTING MACHINERY. 1997: 80–85

  View details for Web of Science ID A1997WE34900008

• Adding Type Parameterization to the Java Language. Agesen, O., Freund, Stephen, N., Mitchell, John, C. 1997
• Automated analysis of cryptographic protocols using Mur-phi. Mitchell, John, C., Mitchell, M., Stern, U. 1997
• The analysis of programming structure. SIGACT News Mitchell, John, C., Riecke, Jon, G. 1997; 2 (28): 24-31
• A Type System For Object Initialization In the Java Bytecode Language. Electr. Notes Theor. Comput. Sci. Freund, Stephen, N., Mitchell, John, C. 1997; 10: 242-245
• Strategic directions in software engineering and programming languages ACM COMPUTING SURVEYS Gunter, C., Mitchell, J., Notkin, D. 1996; 28 (4): 727-737

  View details for Web of Science ID A1996WT68000012

• Standard ML-NJ weak polymorphism and imperative constructs 8TH ANNUAL IEEE SYMP ON LOGIC IN COMPUTER SCIENCE ( LICS 93 ) Mitchell, J., Viswanathan, R. ACADEMIC PRESS INC ELSEVIER SCIENCE. 1996: 102–16

  View details for Web of Science ID A1996UY89000004

• Linear logic proof games and optimization. Bulletin of Symbolic Logic Lincoln, P., Mitchell, John, C., Scedrov, A. 1996; 3 (2): 322-338
• The Complexity of Local Proof Search in Linear Logic. Electr. Notes Theor. Comput. Sci. Lincoln, P., Mitchell, John, C., Scedrov, A. 1996; 3: 120-129
• ML and Beyond. ACM Comput. Surv. Harper, R., Mitchell, John, C. 1996; 4es (28): 219
• Effective Models of Polymorphism, Subtyping and Recursion (Extended Abstract). Mitchell, John, C., Viswanathan, R. 1996
• Foundations for programming languages. Mitchell, John, C. Foundation of computing series, MIT Press. 1996
• The Development of Type Systems for Object-Oriented Languages. TAPOS Fisher, K., Mitchell, John, C. 1995; 3 (1): 189-220
• A Delegation-based Object Calculus with Subtying. Fisher, K., Mitchell, John, C. 1995
• Lower Bounds on Type Inference with Subtypes. Hoang, M., Mitchell, John, C. 1995
• POLYMORPHISM AND SUBTYPING IN INTERFACES Workshop on Interface Definition Languages/1994 ACM Symposium on Principles of Programming Languages Katiyar, D., LUCKHAM, D., Mitchell, J., Meldal, S. ASSOC COMPUTING MACHINERY. 1994: 22–34

  View details for Web of Science ID A1994NY41900004

• AN EXTENSION OF SYSTEM-F WITH SUBTYPING 1st International Conference on Theoretical Aspects of Computer Software (TACS 91) Cardelli, L., Martini, S., Mitchell, J. C., Scedrov, A. ACADEMIC PRESS INC JNL-COMP SUBSCRIPTIONS. 1994: 4–56

  View details for Web of Science ID A1994NF09800002

• Polymorphism and Subtyping in Interfaces. Katiyar, D., Luckham, David, C., Mitchell, John, C. 1994
• A Type System for Prototyping Languages. Katiyar, D., Luckham, David, C., Mitchell, John, C. 1994
• A lambda Calculus of Objects and Method Specialization. Nord. J. Comput. Fisher, K., Honsell, F., Mitchell, John, C. 1994; 1 (1): 3-37
• An Extension of System F with Subtyping. Inf. Comput. Cardelli, L., Martini, S., Mitchell, John, C., Scedrov, A. 1994; 1/2 (109): 4-56
• Notes on Typed Object-Oriented Programming. Fisher, K., Mitchell, John, C. 1994
• ON ABSTRACTION AND THE EXPRESSIVE POWER OF PROGRAMMING-LANGUAGES SCIENCE OF COMPUTER PROGRAMMING Mitchell, J. C. 1993; 21 (2): 141-163

  View details for Web of Science ID A1993MH81400004

• ON THE TYPE-STRUCTURE OF STANDARD ML ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS Harper, R., Mitchell, J. C. 1993; 15 (2): 211-252

  View details for Web of Science ID A1993LQ58900001

• On Abstraction and the Expressive Power of Programming Languages. Sci. Comput. Program. Mitchell, John, C. 1993; 2 (21): 141-163
• STANDARD ML-NJ WEAK POLYMORPHISM AND IMPERATIVE CONSTRUCTS 8TH ANNUAL IEEE SYMP ON LOGIC IN COMPUTER SCIENCE ( LICS 93 ) Hoang, M., Mitchell, J., Viswanathan, R. I E E E, COMPUTER SOC PRESS. 1993: 15–25

  View details for Web of Science ID A1993BY60N00003

• On the Type Structure of Standard ML. ACM Trans. Program. Lang. Syst. Harper, R., Mitchell, John, C. 1993; 2 (15): 211-252
• Standard ML-NJ weak polymorphism and imperative constructs. Hoang, M., Mitchell, John, C. 1993
• Type Inference with Extended Pattern Matching and Subtypes. Fundam. Inform. Jategaonkar, L., Mitchell, John, C. 1993; 1/2 (19): 127-165
• A lambda calculus of objects and method specialization. Mitchell, John, C., Honsell, F., Fisher, K. 1993
• DECISION-PROBLEMS FOR PROPOSITIONAL LINEAR LOGIC ANNALS OF PURE AND APPLIED LOGIC Lincoln, P., Mitchell, J., Scedrov, A., Shankar, N. 1992; 56 (1-3): 239-311

  View details for Web of Science ID A1992HW52000012

• CONNECTING FORMAL SEMANTICS TO CONSTRUCTIVE INTUITIONS 1991 SUMMER SYMP ON CONSTRUCTIVITY IN COMPUTER SCIENCE Kurtz, S. A., Mitchell, J. C., Odonnell, M. J. SPRINGER VERLAG. 1992: 1–21

  View details for Web of Science ID A1992LE88400002

• OPERATIONAL ASPECTS OF LINEAR LAMBDA-CALCULUS 7TH ANNUAL SYMP ON LOGIC IN COMPUTER SCIENCE ( LICS 92 ) Lincoln, P., Mitchell, J. I E E E, COMPUTER SOC PRESS. 1992: 235–246

  View details for Web of Science ID A1992BW24D00023

• Algorithmic Aspects of Type Inference with Subtypes. Lincoln, P., Mitchell, John, C. 1992
• Operational aspects of linear lambda calculus. Lincoln, P., Mitchell, John, C. 1992
• PER Models of Subtyping, Recursive Types and Higher-Order Polymorphism. Bruce, Kim, B., Mitchell, John, C. 1992
• Notes on Sconing and Relators. Mitchell, John, C., Scedrov, A. 1992
• Decision Problems for Propositional Linear Logic. Ann. Pure Appl. Logic Lincoln, P., Mitchell, John, C. 1992; 1-3 (56): 239-311
• KRIPKE-STYLE MODELS FOR TYPED LAMBDA-CALCULUS 2ND ANNUAL SYMP ON LOGIC IN COMPUTER SCIENCE Mitchell, J. C., Moggi, E. ELSEVIER SCIENCE BV. 1991: 99–124

  View details for Web of Science ID A1991FD94000004

• ON ABSTRACTION AND THE EXPRESSIVE POWER OF PROGRAMMING-LANGUAGES LECTURE NOTES IN COMPUTER SCIENCE Mitchell, J. C. 1991; 526: 290-310

  View details for Web of Science ID A1991GJ61000015

• AN EXTENSION OF SYSTEM-F WITH SUBTYPING LECTURE NOTES IN COMPUTER SCIENCE Cardelli, L., Martini, S., Mitchell, J. C., Scedrov, A. 1991; 526: 750-770

  View details for Web of Science ID A1991GJ61000037

• An Extension of Standard ML Modules with Subtyping and Inheritance. Mitchell, John, C., Meldal, S., Madhav, N. 1991
• Connecting Formal Semantics to Constructive Intuitions. Kurtz, Stuart, A., Mitchell, John, C., O'Donnell, Michael, J. 1991
• Unification and ML-Type Reconstruction. Computational Logic - Essays in Honor of Alan Robinson Kanellakis, Paris, C., Mairson, Harry, G., Mitchell, John, C. 1991: 444–478
• An Extension of System F with Subtyping. Cardelli, L., Martini, S., Mitchell, John, C. 1991
• Type Inference With Simple Subtypes. J. Funct. Program. Mitchell, John, C. 1991; 3 (1): 245-285
• On Abstraction and the Expressive Power of Programming Languages. Mitchell, John, C. 1991
• Operations on Records. Mathematical Structures in Computer Science Cardelli, L., Mitchell, John, C. 1991; 1 (1): 3-48
• Kripke-Style Models for Typed lambda Calculus. Ann. Pure Appl. Logic Mitchell, John, C., Moggi, E. 1991; 1-2 (51): 99-124
• AN EXTENSION OF SYSTEM-F WITH SUBTYPING INTERNATIONAL CONF ON THEORETICAL ASPECTS OF COMPUTER SOFTWARE ( TACS 91 ) Cardelli, L., Martini, S., Mitchell, J. C., Scedrov, A. SPRINGER-VERLAG BERLIN. 1991: 750–770

  View details for Web of Science ID A1991BU27Y00037

• THE SEMANTICS OF 2ND-ORDER LAMBDA CALCULUS INFORMATION AND COMPUTATION Bruce, K. B., Meyer, A. R., Mitchell, J. C. 1990; 85 (1): 76-134

  View details for Web of Science ID A1990CV31300003

• OPERATIONS ON RECORDS 5TH INTERNATIONAL CONF ON MATHEMATICAL FOUNDATIONS OF PROGRAMMING SEMANTICS Cardelli, L., Mitchell, J. C. SPRINGER-VERLAG BERLIN. 1990: 22–52

  View details for Web of Science ID A1990BR79W00003

• TOWARD A TYPED FOUNDATION FOR METHOD SPECIALIZATION AND INHERITANCE MITCHELL, J. C., ASSOC COMP MACHINERY ASSOC COMPUTING MACHINERY. 1990: 109–24

  View details for Web of Science ID A1990BR03H00009

• DECISION-PROBLEMS FOR PROPOSITIONAL LINEAR LOGIC 31ST ANNUAL SYMP ON FOUNDATIONS OF COMPUTER SCIENCE Lincoln, P., Mitchell, J., Scedrov, A., Shankar, N. I E E E, COMPUTER SOC PRESS. 1990: 662–671

  View details for Web of Science ID A1990BS19T00069

• HIGHER-ORDER MODULES AND THE PHASE DISTINCTION 17TH ANNUAL SYMP OF THE ASSOC FOR COMPUTING MACHINERY : PRINCIPLES OF PROGRAMMING LANGUAGES Harper, R., Mitchell, J. C., Moggi, E. ASSOC COMPUTING MACHINERY. 1990: 341–354

  View details for Web of Science ID A1990BR03H00028

• Higher-Order Modules and the Phase Distinction. Harper, R., Mitchell, John, C., Moggi, E. 1990
• Decision Problems for Propositional Linear Logic. Lincoln, P., Mitchell, John, C., Scedrov, A., Shankar, N. 1990
• Type Systems for Programming Languages. Handbook of Theoretical Computer Science, Volume B: Formal Models and Sematics (B) Mitchell, John, C. 1990: 365-458
• Toward a Typed Foundation for Method Specialization and Inheritance. Mitchell, John, C. 1990
• Operational and Axiomatic Semantics of PCF. Howard, Brian, T., Mitchell, John, C. 1990
• The Semantics of Second-Order Lambda Calculus. Inf. Comput. Bruce, Kim, B., Meyer, Albert, R., Mitchell, John, C. 1990; 1 (85): 76-134
• OPERATIONS ON RECORDS LECTURE NOTES IN COMPUTER SCIENCE Cardelli, L., Mitchell, J. C. 1989; 389: 75-81

  View details for Web of Science ID A1989AV19900005

• Operations on Records. Cardelli, L., Mitchell, John, C. 1989
• F-Bounded Polymorphism for Object-Oriented Programming. Canning, Peter, S., Cook, William, R., Hill, Walter, L., Olthoff, Walter, G., Mitchell, John, C. 1989
• Polymorphic Unification and ML Typing. Kanellakis, Paris, C., Mitchell, John, C. 1989
• Operations in Records. Cardelli, L., Mitchell, John, C. 1989
• ABSTRACT TYPES HAVE EXISTENTIAL TYPE ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS Mitchell, J. C., Plotkin, G. D. 1988; 10 (3): 470-502

  View details for Web of Science ID A1988P815300006

• Polymorphic Type Inference and Containment. Inf. Comput. Mitchell, John, C. 1988; 2/3 (76): 211-249
• ML with Extended Pattern Matching and Subtypes. Jategaonkar, L., Mitchell, John, C. 1988
• The Essence of ML. Mitchell, John, C., Harper, R. 1988
• Empty Types in Polymorphic Lambda Calculus. Meyer, Albert, R., Mitchell, John, C., Moggi, E., Statman, R. 1987
• Kripke-Style models for typed lambda calculus. Mitchell, John, C., Moggi, E. 1987
• Representation Independence and Data Abstraction. Mitchell, John, C. 1986
• Realisability Semantics for Error-Tolerant Logics. Mitchell, John, C., O'Donnell, Michael, J. 1986
• A Type-Inference Approach to Reduction Properties and Semantics of Polymorphic Expressions (Summary). Mitchell, John, C. 1986
• Abstract Types Have Existential Type. Mitchell, John, C., Plotkin, Gordon, D. 1985
• Second-Order Logical Relations (Extended Abstract). Mitchell, John, C., Meyer, Albert, R. 1985
• Semantic Models for Second-Order Lambda Calculus. Mitchell, John, C. 1984
• Coercion and Type Inference. Mitchell, John, C. 1984
• On the Sequential Nature of Unification. J. Log. Program. Dwork, C., Kanellakis, Paris, C., Mitchell, John, C. 1984; 1 (1): 35-50
• The Implication Problem for Functional and Inclusion Dependencies. Information and Control Mitchell, John, C. 1983; 3 (56): 154-173
• Termination Assertions for Recursive Programs: Completeness and Axiomatic Definability. Information and Control Meyer, Albert, R., Mitchell, John, C. 1983; 1/2 (56): 112-138
• Inference Rules for Functional and Inclusion Dependencies. Mitchell, John, C. 1983
• Axiomatic Definability and Completeness for Recursive Programs. Meyer, Albert, R., Mitchell, John, C. 1982