John Mitchell
Mary and Gordon Crary Family Professor in the School of Engineering, and Professor, by courtesy, of Electrical Engineering and of Education
Computer Science
Bio
John Mitchell is the Mary and Gordon Crary Family Professor, professor of computer science, and by courtesy professor of electrical engineering and professor of education. He was previously Stanford Vice Provost for Teaching and Learning and chair of the Computer Science Department. As vice provost, his team worked with more than 500 Stanford faculty members and instructors on over 1,000 online projects for campus or public audiences and organized the Year of Learning to envision the future of teaching and learning at Stanford and beyond. As co-director of the Lytics Lab, Carta Lab and Pathways Lab, he has worked to improve educational outcomes through data-driven research and iterative design.
Mitchell’s research focusses on programming languages, computer security and privacy, blockchain, machine learning, and technology for education. Sample publications include Reinforcement Learning for the Adaptive Scheduling of Educational Activities (CHI 2020), Automated Analysis of Cryptographic Assumptions in Generic Group Models (J. Cryptology, 2019), Evaluating the privacy properties of telephone metadata (PNAS 2016), and Third-party web tracking: Policy and Technology (IEEE S&P). He is the author of two textbooks, Foundations for Programming Languages (1996) and Concepts in Programming Languages (2002). With over 250 publications and over 30,000 citations, he has led research projects on a range of topics, been a consultant or advisor to many companies, and served as editor-in-chief of the Journal of Computer Security.
Mitchell’s first research project in online learning started in 2009, when he and six undergraduate students built Stanford CourseWare, an innovative platform that expanded to support interactive video and discussion. CourseWare served as the foundation for initial flipped classroom experiments at Stanford and helped inspire the first massive open online courses (MOOCs) from Stanford.
Academic Appointments
-
Professor, Computer Science
-
Professor (By courtesy), Electrical Engineering
-
Professor (By courtesy), Graduate School of Education
-
Faculty Affiliate, Institute for Human-Centered Artificial Intelligence (HAI)
Administrative Appointments
-
Chair, Department of Computer Science (2019 - Present)
Honors & Awards
-
Mary and Gordon Crary Family Professor in the School of Engineering, Stanford University
-
Elected, American Academy of Arts and Sciences
-
Fellow, Association for Computing Machinery
Professional Education
-
BS, Stanford Univeristy, Mathematics (1978)
-
PhD, MIT, Computer Science (1984)
Research Interests
-
Higher Education
-
Teachers and Teaching
-
Technology and Education
Current Research and Scholarly Interests
Programming languages, computer security and privacy, blockchain, machine learning, and technology for education
2024-25 Courses
- How Can Generative AI Help Us Learn?
CS 53N (Spr) - Trustworthy Machine Learning
CS 329T (Aut) -
Independent Studies (19)
- Advanced Reading and Research
CS 499 (Aut, Win, Spr) - Advanced Reading and Research
CS 499P (Aut, Win, Spr) - Curricular Practical Training
CS 390A (Aut, Win, Spr) - Curricular Practical Training
CS 390B (Aut, Win, Spr) - Curricular Practical Training
CS 390C (Aut, Win, Spr) - Independent Project
CS 399 (Aut, Win, Spr) - Independent Project
CS 399P (Aut, Win, Spr) - Independent Work
CS 199 (Aut, Win, Spr) - Independent Work
CS 199P (Aut, Win, Spr) - Master's Thesis and Thesis Research
EE 300 (Aut, Win, Spr) - Part-time Curricular Practical Training
CS 390D (Aut, Win, Spr) - Programming Service Project
CS 192 (Aut, Win, Spr) - Senior Project
CS 191 (Aut, Win, Spr) - Special Studies and Reports in Electrical Engineering
EE 191 (Aut, Win, Spr) - Special Studies and Reports in Electrical Engineering
EE 391 (Aut, Win, Spr) - Special Studies or Projects in Electrical Engineering
EE 190 (Aut, Win, Spr) - Special Studies or Projects in Electrical Engineering
EE 390 (Aut, Win, Spr) - Supervised Undergraduate Research
CS 195 (Aut, Win, Spr) - Writing Intensive Senior Research Project
CS 191W (Aut, Win, Spr)
- Advanced Reading and Research
-
Prior Year Courses
2023-24 Courses
- Design for Learning: Generative AI for Collaborative Learning
CS 498D, DESIGN 292, EDUC 449 (Aut) - How Can Generative AI Help Us Learn?
CS 53N (Spr) - Trustworthy Machine Learning
CS 329T (Aut)
2022-23 Courses
- Design for Learning: Co-Designing Connection and Community
DESIGN 292 (Aut)
2021-22 Courses
- Trustworthy Machine Learning
CS 329T (Spr)
- Design for Learning: Generative AI for Collaborative Learning
Stanford Advisees
-
Doctoral Dissertation Advisor (AC)
Jeongyeon Kim -
Doctoral Dissertation Co-Advisor (AC)
Paul Crews, Jason Goldberg -
Master's Program Advisor
Roman Gasiorowski, Jeremy Kim, Calvin Laughlin, Sean Mori, Ihyun Nam, Ayush Singla, Ari Webb -
Doctoral (Program)
Jeongyeon Kim, Sierra Wang
All Publications
-
Remote Learning and Work
IEEE INTERNET COMPUTING
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
2023: 2023
View details for DOI 10.1145/3545945.3569763
-
Insights for post-pandemic pedagogy across one CS department
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
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
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
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
2021: 291-293
View details for DOI 10.1145/3430895.3460161
-
Simplifying Automated Assessment in CS1
International Conference on Education Technology Management
2021: 226-231
View details for DOI 10.1145/3510309.3510345
- Model Checking Bitcoin and other Proof-of-Work Consensus Protocols 2020 IEEE International Conference on Blockchain. 2020
-
Model Checking Bitcoin and other Proof-of-Work Consensus Protocols
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
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 IEEE Learning With MOOCS (LWMOOCS). 2020
- Reinforcement Learning for the Adaptive Scheduling of Educational Activities Proc 2020 CHI Conference on Human Factors in Computing Systems. 2020
-
Automated Analysis of Cryptographic Assumptions in Generic Group Models
JOURNAL OF CRYPTOLOGY
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
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
2017; 27
View details for DOI 10.1017/S0956796816000241
View details for Web of Science ID 000393984200001
-
Privacy for Targeted Advertising
IEEE. 2017: 438–43
View details for Web of Science ID 000426981000067
-
Hails: Protecting data privacy in untrusted web applications
JOURNAL OF COMPUTER SECURITY
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
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
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
AUAI PRESS. 2015: 672–81
View details for Web of Science ID 000493121100069
-
Automated Analysis of Cryptographic Assumptions in Generic Group Models
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
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. 2013
- Compressive Feature Learning. 2013
-
Addressing Covert Termination and Timing Channels in Concurrent Information Flow Systems
ACM SIGPLAN NOTICES
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
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
2012; 100: 1659-1673
View details for DOI 10.1109/JPROC.2012.2189794
View details for Web of Science ID 000309838000049
- Third-Party Web Tracking: Policy and Technology. 2012
-
Disjunction Category Labels
16th Nordic Conference on Secure IT-Systems (NordSec)
SPRINGER-VERLAG BERLIN. 2012: 223–239
View details for Web of Science ID 000310342000016
-
Third-Party Web Tracking: Policy and Technology
33rd IEEE Symposium on Security and Privacy (SP)
IEEE. 2012: 413–427
View details for DOI 10.1109/SP.2012.47
View details for Web of Science ID 000309219900027
-
Information-flow control for programming on encrypted data
25th IEEE Computer Security Foundations Symposium (CSF)
IEEE. 2012: 45–60
View details for DOI 10.1109/CSF.2012.30
View details for Web of Science ID 000309007800004
- SessionJuggler: secure web login from an untrusted terminal using session hijacking. 2012
- Addressing covert termination and timing channels in concurrent information flow systems. 2012
- Declarative privacy policy: finite models and attribute-based encryption. 2012
- Information-Flow Control for Programming on Encrypted Data. 2012
- Information-flow control for programming on encrypted data. IACR Cryptology ePrint Archive 2012: 205
- Flexible Dynamic Information Flow Control in the Presence of Exceptions. CoRR abs/1207.1457 2012
-
Flexible Dynamic Information Flow Control in Haskell
ACM SIGPLAN NOTICES
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
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
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. 2011
-
Flexible Dynamic Information Flow Control in Haskell
ASSOC COMPUTING MACHINERY. 2011: 95–106
View details for Web of Science ID 000304130300009
-
Program Analysis for Web Security
SPRINGER-VERLAG BERLIN. 2011: 4
View details for Web of Science ID 000306978900003
-
Text-based CAPTCHA Strengths and Weaknesses
ASSOC COMPUTING MACHINERY. 2011: 125–37
View details for Web of Science ID 000397423700012
-
A Domain-Specific Language for Computing on Encrypted Data
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)
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)
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)
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)
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. 2011
- The Failure of Noise-Based Non-continuous Audio Captchas. 2011
- Program Analysis for Web Security. 2011
- Disjunction Category Labels. 2011
- Reclaiming the Blogosphere, TalkBack: A Secure LinkBack Protocol for Weblogs. 2011
- Text-based CAPTCHA strengths and weaknesses. 2011
- TBA : A Hybrid of Logic and Extensional Access Control Systems. Formal Aspects in Security and Trust 2011
- A Domain-Specific Language for Computing on Encrypted Data. IACR Cryptology ePrint Archive 2011: 561
- Inductive trace properties for computational security. Journal of Computer Security 2010; 6 (18): 1035-1073
-
Inductive trace properties for computational security
JOURNAL OF COMPUTER SECURITY
2010; 18 (6): 1035–73
View details for DOI 10.3233/JCS-2009-389
View details for Web of Science ID 000210967900004
-
A Learning-Based Approach to Reactive Security
14th Financial Cryptography and Data Security International Conference
SPRINGER-VERLAG BERLIN. 2010: 192–206
View details for Web of Science ID 000286416700016
-
State of the Art: Automated Black-Box Web Application Vulnerability Testing
Symposium on Security and Privacy
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
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
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
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 2010: 115
- A Learning-Based Approach to Reactive Security. Financial Cryptography 2010
- A Security Evaluation of DNSSEC with NSEC3. 2010
- How Good Are Humans at Solving CAPTCHAs? A Large Scale Evaluation. 2010
- State of the Art: Automated Black-Box Web Application Vulnerability Testing. 2010
- Object Capabilities and Isolation of Untrusted Web Applications. 2010
- Towards a Formal Foundation of Web Security. 2010
-
Using Strategy Objectives for Network Security Analysis
5th China International Conference on Information Security and Cryptology
SPRINGER-VERLAG BERLIN. 2010: 337–349
View details for Web of Science ID 000286442600025
-
A 4-Year Prospective Study of Eating Disorder NOS Compared with Full Eating Disorder Syndromes
INTERNATIONAL JOURNAL OF EATING DISORDERS
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
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
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. 2009
-
Isolating JavaScript with Filters, Rewriting, and Wrappers
COMPUTER SECURITY - ESORICS 2009, PROCEEDINGS
2009; 5789: 505-?
View details for Web of Science ID 000274011000031
- A Formalization of HIPAA for a Medical Messaging System. 2009
- A Learning-Based Approach to Reactive Security. CoRR abs/0912.1155 2009
- Practical declarative network management. 2009
- TrackBack spam: abuse and prevention. 2009
- An Automated Approach for Proving PCL Invariants. Electr. Notes Theor. Comput. Sci. 2009; 234: 93-113
- Using Strategy Objectives for Network Security Analysis. 2009
-
On the relationships between notions of simulation-based security
JOURNAL OF CRYPTOLOGY
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. 2008
-
A Layered Architecture for Detecting Malicious Behaviors
RECENT ADVANCES IN INTRUSION DETECTION, RAID 2008
2008; 5230: 78-?
View details for Web of Science ID 000260067900005
-
An Operational Semantics for JavaScript
PROGRAMMING LANGUAGES AND SYSTEMS, PROCEEDINGS
2008; 5356: 307-?
View details for Web of Science ID 000262126200022
- Analysis of EAP-GPSK Authentication Protocol. 2008
- Securing Frame Communication in Browsers. 2008
- An Operational Semantics for JavaScript. 2008
- Robust defenses for cross-site request forgery. 2008
- Characterizing Bots' Remote Control Behavior. Botnet Detection 2008: 45-64
- Towards Systematic Evaluation of the Evadability of Bot/Botnet Detection Methods. 2008
-
Protocol Composition Logic (PCL)
ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE
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. 2007
- Protocol Composition Logic (PCL). Electr. Notes Theor. Comput. Sci. 2007; 172: 311-358
- Inductive Proof Method for Computational Secrecy. IACR Cryptology ePrint Archive 2007: 165
- Privacy and Utility in Business Processes. 2007
- Formal Proofs of Cryptographic Security of Diffie-Hellman-Based Protocols. 2007
- Inductive Proofs of Computational Secrecy. 2007
-
Compositional analysis of contract-signing protocols
2nd Workshop on Automated Reasoning for Security Protocol Analysis
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
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. 2006
- Secrecy Analysis in Protocol Composition Logic. 2006
- Protecting browser state from web privacy attacks. 2006
- Computationally Sound Compositional Logic for Key Exchange Protocols. 2006
- Inductive Trace Properties for Computational Security. IACR Cryptology ePrint Archive 2006: 486
- On the Relationships Between Notions of Simulation-Based Security. IACR Cryptology ePrint Archive 2006: 153
- Understanding SPKI/SDSI using first-order logic. Int. J. Inf. Sec. 2006; 1 (5): 48-64
- Managing Digital Rights using Linear Logic. 2006
- Privacy and Contextual Integrity: Framework and Applications. 2006
- Key Exchange Protocols: Security Definition, Proof Method and Applications. IACR Cryptology ePrint Archive 2006: 56
-
Contract signing, optimism, and advantage
JOURNAL OF LOGIC AND ALGEBRAIC PROGRAMMING
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
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)
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
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
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. 2005
- A modular correctness proof of IEEE 802.11i and TLS. 2005
- A derivation system and compositional logic for security protocols. Journal of Computer Security 2005; 3 (13): 423-482
- Compositional Analysis of Contract Signing Protocols. 2005
- Security analysis of network protocols: logical and computational methods. 2005
- Games and the Impossibility of Realizable Ideal Functionality. IACR Cryptology ePrint Archive 2005: 211
- Security Analysis and Improvements for IEEE 802.11i. 2005
- On the Relationships Between Notions of Simulation-Based Security. 2005
- Enterprise privacy promises and enforcement. 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 2004; 2 (12): 247-311
- Client-Side Defense Against Web-Based Identity Theft. 2004
- A Distributed High Assurance Reference Monitor. 2004
- Probabilistic Bisimulation and Equivalence for Security Analysis of Network Protocols. 2004
- Reconstructing Trust Management. Journal of Computer Security 2004; 1 (12): 131-164
- Analysis of the 802.11i 4-way handshake. 2004
- Conflict and combination in privacy policy languages. 2004
- Securing Java RMI-Based Distributed Applications. 2004
- Abstraction and Refinement in Protocol Derivation. 2004
-
Development of investigational radiation modifiers
JOURNAL OF THE NATIONAL CANCER INSTITUTE
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
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 2003; 1 (11): 35-86
- A Derivation System for Security Protocols and its Logical Formalization. 2003
- Understanding SPKI/SDSI Using First-Order Logic. 2003
- Beyond Proof-of-Compliance: Safety and Availability Analysis in Trust Management. 2003
- Concepts in programming languages. Cambridge University Press. 2003
- Security by typing. STTT 2003; 4 (4): 472-495
- Contract Signing, Optimism, and Advantage. 2003
- Specifying and Verifying Hardware for Tamper-Resistant Software. 2003
- Secure protocol composition. 2003
- DATALOG with Constraints: A Foundation for Trust Management Languages. 2003
- A Role-based Trust-management Framework. 2003
- Composition of Cryptographic Protocols in a Probabilistic Polynomial-Time Process Calculus. 2003
- Relating cryptography and formal methods: a panel. 2003
- A Compositional Logic for Proving Security Properties of Protocols. Journal of Computer Security 2003; 4 (11): 677-722
-
Finite-state analysis of two contract signing protocols
THEORETICAL COMPUTER SCIENCE
2002; 283 (2): 419-450
View details for Web of Science ID 000176538500006
- Autonomous Nodes and Distributed Mechanisms. 2002
-
Multiset rewriting and security protocol analysis
REWRITING TECHNIQUES AND APPLICATIONS
2002; 2378: 19-22
View details for Web of Science ID 000180069300002
- Design of a Role-Based Trust-Management Framework. 2002
- A Comparison between Strand Spaces and Multiset Rewriting for Security Protocol Analysis. 2002
- Multiset Rewriting and Security Protocol Analysis. 2002
-
Programming language methods in computer security
28th ACM/SIGPLAN/SIGACT Symposium on Principles of Programming Languages (POPL 2001)
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. 2001; 45: 280-310
- Distributed credential chain discovery in trust management: extended abstract. 2001
- Programming language methods in computer security. 2001
- Probabilistic Polynominal-Time Process Calculus and Security Protocol Analysis. 2001
- Probabilistic Polynomial-Time Process Calculus and Security Protocol Analysis. 2001
- A State-Transition Model of Trust Management and Access Control. 2001
- A Compositional Logic for Protocol Correctness. 2001
-
Architectural support for copy and tamper resistant software
9th International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS_IX)
ASSOC COMPUTING MACHINERY. 2000: 168–77
View details for Web of Science ID 000165257200017
- Analysis of Abuse-Free Contract Signing. Financial Cryptography 2000
- Analysis of a Fair Exchange Protocol. 2000
- Relating Strands and Multiset Rewriting for Security Protocol Analysis. 2000
-
A type system for object initialization in the Java bytecode language
ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS
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
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
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
1999; 70 (1): 1-5
View details for Web of Science ID 000080537800001
- Probabilistic Polynomial-Time Equivalence and Security Analysis. 1999
- A Meta-Notation for Protocol Analysis. 1999
- The type system for object initializatiion in the Jave bytecode language. ACM Trans. Program. Lang. Syst. 1999; 6 (21): 1196-1250
- A Formal Framework for the Java Bytecode Language and Verifier. 1999
- A Core Calculus of Classes and Objects. Electr. Notes Theor. Comput. Sci. 1999; 20: 28-49
-
A type system for object initialization in the Java (TM) bytecode language
ACM SIGPLAN NOTICES
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
JOHN WILEY & SONS INC. 1998: 3–25
View details for Web of Science ID 000074393400002
- A Probabilistic Poly-Time Framework for Protocol Analysis. 1998
- A Type System for Object Initialization in the Java Bytecode Language. 1998
- Finite-State Analysis of Security Protocols. 1998
- A Linguistic Characterization of Bounded Oracle Computation and Probabilistic Polynomial Time. 1998
-
Adding type parameterization to the Java(TM) language
1997 ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages and Applications (OOPSLA 97)
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
ASSOC COMPUTING MACHINERY. 1997: 80–85
View details for Web of Science ID A1997WE34900008
- Adding Type Parameterization to the Java Language. 1997
- Automated analysis of cryptographic protocols using Mur-phi. 1997
- The analysis of programming structure. SIGACT News 1997; 2 (28): 24-31
- A Type System For Object Initialization In the Java Bytecode Language. Electr. Notes Theor. Comput. Sci. 1997; 10: 242-245
-
Strategic directions in software engineering and programming languages
ACM COMPUTING SURVEYS
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 )
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 1996; 3 (2): 322-338
- The Complexity of Local Proof Search in Linear Logic. Electr. Notes Theor. Comput. Sci. 1996; 3: 120-129
- ML and Beyond. ACM Comput. Surv. 1996; 4es (28): 219
- Effective Models of Polymorphism, Subtyping and Recursion (Extended Abstract). 1996
- Foundations for programming languages. Foundation of computing series, MIT Press. 1996
- The Development of Type Systems for Object-Oriented Languages. TAPOS 1995; 3 (1): 189-220
- A Delegation-based Object Calculus with Subtying. 1995
- Lower Bounds on Type Inference with Subtypes. 1995
-
POLYMORPHISM AND SUBTYPING IN INTERFACES
Workshop on Interface Definition Languages/1994 ACM Symposium on Principles of Programming Languages
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)
ACADEMIC PRESS INC JNL-COMP SUBSCRIPTIONS. 1994: 4–56
View details for Web of Science ID A1994NF09800002
- Polymorphism and Subtyping in Interfaces. 1994
- A Type System for Prototyping Languages. 1994
- A lambda Calculus of Objects and Method Specialization. Nord. J. Comput. 1994; 1 (1): 3-37
- An Extension of System F with Subtyping. Inf. Comput. 1994; 1/2 (109): 4-56
- Notes on Typed Object-Oriented Programming. 1994
-
ON ABSTRACTION AND THE EXPRESSIVE POWER OF PROGRAMMING-LANGUAGES
SCIENCE OF COMPUTER PROGRAMMING
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
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. 1993; 2 (21): 141-163
-
STANDARD ML-NJ WEAK POLYMORPHISM AND IMPERATIVE CONSTRUCTS
8TH ANNUAL IEEE SYMP ON LOGIC IN COMPUTER SCIENCE ( LICS 93 )
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. 1993; 2 (15): 211-252
- Standard ML-NJ weak polymorphism and imperative constructs. 1993
- Type Inference with Extended Pattern Matching and Subtypes. Fundam. Inform. 1993; 1/2 (19): 127-165
- A lambda calculus of objects and method specialization. 1993
-
DECISION-PROBLEMS FOR PROPOSITIONAL LINEAR LOGIC
ANNALS OF PURE AND APPLIED LOGIC
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
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 )
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. 1992
- Operational aspects of linear lambda calculus. 1992
- PER Models of Subtyping, Recursive Types and Higher-Order Polymorphism. 1992
- Notes on Sconing and Relators. 1992
- Decision Problems for Propositional Linear Logic. Ann. Pure Appl. Logic 1992; 1-3 (56): 239-311
-
KRIPKE-STYLE MODELS FOR TYPED LAMBDA-CALCULUS
2ND ANNUAL SYMP ON LOGIC IN COMPUTER SCIENCE
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
1991; 526: 290-310
View details for Web of Science ID A1991GJ61000015
-
AN EXTENSION OF SYSTEM-F WITH SUBTYPING
LECTURE NOTES IN COMPUTER SCIENCE
1991; 526: 750-770
View details for Web of Science ID A1991GJ61000037
- An Extension of Standard ML Modules with Subtyping and Inheritance. 1991
- Connecting Formal Semantics to Constructive Intuitions. 1991
- Unification and ML-Type Reconstruction. Computational Logic - Essays in Honor of Alan Robinson 1991: 444–478
- An Extension of System F with Subtyping. 1991
- Type Inference With Simple Subtypes. J. Funct. Program. 1991; 3 (1): 245-285
- On Abstraction and the Expressive Power of Programming Languages. 1991
- Operations on Records. Mathematical Structures in Computer Science 1991; 1 (1): 3-48
- Kripke-Style Models for Typed lambda Calculus. Ann. Pure Appl. Logic 1991; 1-2 (51): 99-124
-
AN EXTENSION OF SYSTEM-F WITH SUBTYPING
INTERNATIONAL CONF ON THEORETICAL ASPECTS OF COMPUTER SOFTWARE ( TACS 91 )
SPRINGER-VERLAG BERLIN. 1991: 750–770
View details for Web of Science ID A1991BU27Y00037
-
THE SEMANTICS OF 2ND-ORDER LAMBDA CALCULUS
INFORMATION AND COMPUTATION
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
SPRINGER-VERLAG BERLIN. 1990: 22–52
View details for Web of Science ID A1990BR79W00003
-
TOWARD A TYPED FOUNDATION FOR METHOD SPECIALIZATION AND INHERITANCE
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
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
ASSOC COMPUTING MACHINERY. 1990: 341–354
View details for Web of Science ID A1990BR03H00028
- Higher-Order Modules and the Phase Distinction. 1990
- Decision Problems for Propositional Linear Logic. 1990
- Type Systems for Programming Languages. Handbook of Theoretical Computer Science, Volume B: Formal Models and Sematics (B) 1990: 365-458
- Toward a Typed Foundation for Method Specialization and Inheritance. 1990
- Operational and Axiomatic Semantics of PCF. 1990
- The Semantics of Second-Order Lambda Calculus. Inf. Comput. 1990; 1 (85): 76-134
-
OPERATIONS ON RECORDS
LECTURE NOTES IN COMPUTER SCIENCE
1989; 389: 75-81
View details for Web of Science ID A1989AV19900005
- Operations on Records. 1989
- F-Bounded Polymorphism for Object-Oriented Programming. 1989
- Polymorphic Unification and ML Typing. 1989
- Operations in Records. 1989
-
ABSTRACT TYPES HAVE EXISTENTIAL TYPE
ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS
1988; 10 (3): 470-502
View details for Web of Science ID A1988P815300006
- Polymorphic Type Inference and Containment. Inf. Comput. 1988; 2/3 (76): 211-249
- ML with Extended Pattern Matching and Subtypes. 1988
- The Essence of ML. 1988
- Empty Types in Polymorphic Lambda Calculus. 1987
- Kripke-Style models for typed lambda calculus. 1987
- Representation Independence and Data Abstraction. 1986
- Realisability Semantics for Error-Tolerant Logics. 1986
- A Type-Inference Approach to Reduction Properties and Semantics of Polymorphic Expressions (Summary). 1986
- Abstract Types Have Existential Type. 1985
- Second-Order Logical Relations (Extended Abstract). 1985
- Semantic Models for Second-Order Lambda Calculus. 1984
- Coercion and Type Inference. 1984
- On the Sequential Nature of Unification. J. Log. Program. 1984; 1 (1): 35-50
- The Implication Problem for Functional and Inclusion Dependencies. Information and Control 1983; 3 (56): 154-173
- Termination Assertions for Recursive Programs: Completeness and Axiomatic Definability. Information and Control 1983; 1/2 (56): 112-138
- Inference Rules for Functional and Inclusion Dependencies. 1983
- Axiomatic Definability and Completeness for Recursive Programs. 1982