Andrew Wilson Appel
Contact Expert

View Scopus Profile

Andrew Wilson Appel

Calculated based on number of publications stored in Pure and citations from Scopus
1985 …2023

Research activity per year

If you made any changes in Pure these will be visible here soon.
Filter
Conference contribution

Search results

  • 2022

    Coq's Vibrant Ecosystem for Verification Engineering (Invited Talk)

    Appel, A. W., Jan 17 2022, CPP 2022 - Proceedings of the 11th ACM SIGPLAN International Conference on Certified Programs and Proofs, co-located with POPL 2022. Popescu, A. & Zdancewic, S. (eds.). Association for Computing Machinery, Inc, p. 2-11 10 p. (CPP 2022 - Proceedings of the 11th ACM SIGPLAN International Conference on Certified Programs and Proofs, co-located with POPL 2022).

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

    Open Access
    1 Scopus citations

  • Verified Erasure Correction in Coq with MathComp and VST

    Cohen, J. M., Wang, Q. & Appel, A. W., 2022, Computer Aided Verification - 34th International Conference, CAV 2022, Proceedings. Shoham, S. & Vizel, Y. (eds.). Springer Science and Business Media Deutschland GmbH, p. 272-292 21 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 13372 LNCS).

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

    Open Access

  • Verified Numerical Methods for Ordinary Differential Equations

    Kellison, A. E. & Appel, A. W., 2022, Software Verification and Formal Methods for ML-Enabled Autonomous Systems - 5th International Workshop, FoMLAS 2022, and 15th International Workshop, NSV 2022, Proceedings. Isac, O., Katz, G., Ivanov, R., Narodytska, N. & Nenzi, L. (eds.). Springer Science and Business Media Deutschland GmbH, p. 147-163 17 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 13466 LNCS).

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

  • 2020

    Connecting Higher-Order Separation Logic to a First-Order Outside World

    Mansky, W., Honoré, W. & Appel, A. W., 2020, Programming Languages and Systems- 29th European Symposium on Programming, ESOP 2020 held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Proceedings. Müller, P. (ed.). Springer, p. 428-455 28 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 12075 LNCS).

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

    Open Access
    4 Scopus citations

  • Verified sequential Malloc/Free

    Appel, A. W. & Naumann, D. A., Jun 16 2020, ISMM 2020 - Proceedings of the 2020 ACM SIGPLAN International Symposium on Memory Management, co-located with PLDI 2020. Ding, C. & Maas, M. (eds.). Association for Computing Machinery, p. 48-59 12 p. (International Symposium on Memory Management, ISMM).

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

    Open Access
    6 Scopus citations
  • 2019

    Abstraction and subsumption in modular verification of C programs

    Beringer, L. & Appel, A. W., 2019, Formal Methods – The Next 30 Years - 3rd World Congress, FM 2019, Proceedings. ter Beek, M. H., McIver, A. & Oliveira, J. N. (eds.). Springer, p. 573-590 18 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 11800 LNCS).

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

    6 Scopus citations
  • 2017

    Bringing order to the separation logic jungle

    Cao, Q., Cuellar, S. & Appel, A. W., 2017, Programming Languages and Systems - 15th Asian Symposium, APLAS 2017, Proceedings. Chang, B-Y. E. (ed.). Springer Verlag, p. 190-211 22 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 10695 LNCS).

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

    10 Scopus citations

  • Shrink fast correctly!

    Bélanger, O. S. & Appel, A. W., Oct 9 2017, Proceedings of the 19th International Symposium on Principles and Practice of Declarative Programming, PPDP 2017. Association for Computing Machinery, p. 49-60 12 p. (ACM International Conference Proceeding Series; vol. Part F131196).

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

    6 Scopus citations

  • Verified correctness and security of mbed TLS HMAC-DRBG

    Ye, K. Q., Green, M., Sanguansin, N., Beringer, L., Petcher, A. & Appel, A. W., Oct 30 2017, CCS 2017 - Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security. Association for Computing Machinery, p. 2007-2020 14 p. (Proceedings of the ACM Conference on Computer and Communications Security).

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

    38 Scopus citations
  • 2016

    Modular verification for computer security

    Appel, A. W., Aug 8 2016, Proceedings - IEEE 29th Computer Security Foundations Symposium, CSF 2016. IEEE Computer Society, 7536361. (Proceedings - IEEE Computer Security Foundations Symposium; vol. 2016-August).

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

    6 Scopus citations
  • 2015

    Compositional comp cert

    Stewart, G., Beringer, L., Cuellar, S. & Appel, A. W., Jan 14 2015, POPL 2015 - Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. Association for Computing Machinery, p. 275-287 13 p. (Conference Record of the Annual ACM Symposium on Principles of Programming Languages; vol. 2015-January).

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

    50 Scopus citations

  • Verification of a cryptographic primitive: SHA-256 (abstract)

    Appel, A. W., Jun 3 2015, PLDI 2015 - Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation. Association for Computing Machinery, Vol. 2015-June. 1 p.

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

    3 Scopus citations

  • Verified correctness and security of OpenSSL HMAC

    Beringer, L., Petcher, A., Ye, K. Q. & Appel, A. W., Jan 1 2015, Proceedings of the 24th USENIX Security Symposium. USENIX Association, p. 207-221 15 p. (Proceedings of the 24th USENIX Security Symposium).

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

    74 Scopus citations
  • 2014

    Portable software fault isolation

    Kroll, J. A., Stewart, G. & Appel, A. W., Nov 13 2014, Proceedings - 2014 IEEE 27th Computer Security Foundations Symposium, CSF 2014. IEEE Computer Society, p. 18-32 15 p. 6957100. (Proceedings of the Computer Security Foundations Workshop; vol. 2014-January).

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

    12 Scopus citations

  • Verified compilation for shared-memory C

    Beringer, L., Stewart, G., Dockins, R. & Appel, A. W., 2014, Programming Languages and Systems - 23rd European Symposium on Programming, ESOP 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Proceedings. Springer Verlag, p. 107-127 21 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 8410 LNCS).

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

    23 Scopus citations
  • 2013

    Mostly sound type system improves a foundational program verifier

    Dodds, J. & Appel, A. W., Dec 1 2013, Certified Programs and Proofs - Third International Conference, CPP 2013, Proceedings. p. 17-32 16 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 8307 LNCS).

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

    2 Scopus citations
  • 2012

    A certificate infrastructure for machine-checked proofs of conditional information flow

    Amtoft, T., Dodds, J., Zhang, Z., Appel, A., Beringer, L., Hatcliff, J., Ou, X. & Cousino, A., 2012, Principles of Security and Trust - First International Conference, POST 2012, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012, Proceedings. p. 369-389 21 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 7215 LNCS).

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

    17 Scopus citations

  • Verified heap theorem prover by paramodulation

    Stewart, G., Beringer, L. & Appel, A. W., 2012, ICFP'12 - Proceedings of the 2012 ACM SIGPLAN International Conference on Functional Programming. p. 3-14 12 p. (Proceedings of the ACM SIGPLAN International Conference on Functional Programming, ICFP).

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

    5 Scopus citations
  • 2011

    Local actions for a curry-style operational semantics

    Stewart, G. & Appel, A. W., 2011, PLPV'11 - Proceedings of the 5th ACM Workshop on Programming Languages Meets Program Verification. p. 31-42 12 p. (PLPV'11 - Proceedings of the 5th ACM Workshop on Programming Languages Meets Program Verification).

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

    2 Scopus citations

  • Verified software toolchain (Invited talk)

    Appel, A. W., 2011, Programming Languages and Systems - 20th European Symposium on Programming, ESOP 2011, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2011, Proceedings. p. 1-17 17 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 6602 LNCS).

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

    Open Access
    92 Scopus citations

  • VeriSmall: Verified smallfoot shape analysis

    Appel, A. W., 2011, Certified Programs and Proofs - First International Conference, CPP 2011, Proceedings. p. 231-246 16 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 7086 LNCS).

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

    7 Scopus citations
  • 2010

    A logical mix of approximation and separation

    Hobor, A., Dockins, R. & Appel, A. W., 2010, Programming Languages and Systems - 8th Asian Symposium, APLAS 2010, Proceedings. p. 439-454 16 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 6461 LNCS).

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

  • A theory of indirection via approximation

    Hobor, A., Dockins, R. & Appel, A. W., 2010, POPL'10 - Proceedings of the 37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. p. 171-184 14 p. (Conference Record of the Annual ACM Symposium on Principles of Programming Languages).

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

    15 Scopus citations

  • Concurrent separation logic for pipelined parallelization

    Bell, C. J., Appel, A. W. & Walker, D., 2010, Static Analysis - 17th International Symposium, SAS 2010, Proceedings. p. 151-166 16 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 6337 LNCS).

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

    12 Scopus citations
  • 2009

    A fresh look at separation algebras and share accounting

    Dockins, R., Hobor, A. & Appel, A. W., Dec 28 2009, Programming Languages and Systems - 7th Asian Symposium, APLAS 2009, Proceedings. p. 161-177 17 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 5904 LNCS).

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

    76 Scopus citations
  • 2008

    Oracle semantics for concurrent separation logic

    Hobor, A., Appel, A. W. & Nardelli, F. Z., 2008, Programming Languages and Systems - 17th European Symposium on Programming, ESOP 2008 - Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Proceedings. p. 353-367 15 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 4960 LNCS).

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

    78 Scopus citations
  • 2007

    A very modal model of a modern, major, general type system

    Appel, A. W., Melliès, P. A., Richards, C. D. & Vouillon, J., 2007, Conference Record of POPL 2007: The 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages - Papers Presented at the Symposium. p. 109-122 14 p. (Conference Record of the Annual ACM Symposium on Principles of Programming Languages).

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

    61 Scopus citations

  • Separation logic for small-step Cminor

    Appel, A. W. & Blazy, S., 2007, Theorem Proving in Higher Order Logics - 20th International Conference, TPHOLs 2007, Proceedings. Springer Verlag, p. 5-21 17 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 4732 LNCS).

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

    56 Scopus citations
  • 2006

    A compositional logic for control flow

    Tan, G. & Appel, A. W., Jul 6 2006, Verification, Model Checking, and Abstract Interpretation - 7th International Conference, VMCAI 2006, Proceedings. p. 80-94 15 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 3855 LNCS).

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

    31 Scopus citations
  • 2004

    Construction of a semantic model for a typed assembly language

    Tan, G., Appel, A. W., Swadi, K. N. & Wu, D., 2004, Verification, Model Checking, and Abstract Interpretation - 5th International Conference, VMCAI 2004, Proceedings. Steffen, B. & Levi, G. (eds.). Springer Verlag, p. 30-43 14 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 2937).

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

    1 Scopus citations
  • 2003

    Access control on the Web using proof-carrying authorization

    Bauer, L., Schneider, M. A., Felten, E. W. & Appel, A. W., Jan 1 2003, Proceedings - DARPA Information Survivability Conference and Exposition, DISCEX 2003. Institute of Electrical and Electronics Engineers Inc., p. 117-119 3 p. 1194942. (Proceedings - DARPA Information Survivability Conference and Exposition, DISCEX 2003; vol. 2).

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

    9 Scopus citations

  • Foundational proof-carrying code

    Appel, A. W., 2003, Foundations of Intrusion Tolerant Systems, OASIS 2003. Lala, J. H. (ed.). Institute of Electrical and Electronics Engineers Inc., p. 25-34 10 p. 1264926. (Foundations of Intrusion Tolerant Systems, OASIS 2003).

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

    2 Scopus citations

  • Foundational Proof Checkers with Small Witnesses

    Wu, D., Appel, A. W. & Stump, A., 2003, Proceedings of the Fifth ACM SIGPLAN Conference on Principle and Practice of Declarative Programming, (PPDP 03). Association for Computing Machinery, p. 264-274 11 p. (Proceedings of the ACM SIGPLAN Conference on Principles and Practice of Declarative Programming; vol. 5).

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

    31 Scopus citations

  • Policy-Enforced Linking of Untrusted Components (Extended Abstract)

    Lee, E. & Appel, A. W., Dec 1 2003, Proceedings of the Joint 9th European Software Engineering Conference (ESEC) and 11th SIGSOFT Symposium on the Foundations of Software Engineering (FSE-11). Inverardi, P. (ed.). p. 371-374 4 p. (Proceedings of the Joint European Software Engineering Conference (ESEC) and SIGSOFT Symposium on the Foundations of Software Engineering (FSE-11)).

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

    2 Scopus citations

  • Using memory errors to attack a virtual machine

    Govindavajhala, S. & Appel, A. W., 2003, Proceedings - 2003 Symposium on Security and Privacy, SP 2003. Institute of Electrical and Electronics Engineers Inc., p. 154-165 12 p. 1199334. (Proceedings - IEEE Symposium on Security and Privacy; vol. 2003-January).

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

    31 Scopus citations
  • 2001

    Foundational proof-carrying code

    Appel, A. W., Jan 1 2001, Proceedings - Symposium on Logic in Computer Science. p. 247-256 10 p.

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

    205 Scopus citations
  • 2000

    Machine instruction syntax and semantics in higher order logic

    Michael, N. G. & Appel, A. W., Jan 1 2000, Automated Deduction - CADE-17 - 17th International Conference on Automated Deduction, Proceedings. McAllester, D. (ed.). Springer Verlag, p. 7-24 18 p. (Lecture Notes in Artificial Intelligence (Subseries of Lecture Notes in Computer Science); vol. 1831).

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

    19 Scopus citations
  • 1997

    Lambda-splitting: A higher-order approach to cross-module optimizations

    Blume, M. & Appel, A. W., Jan 1 1997, Proceedings of the ACM SIGPLAN International Conference on Functional Programming, ICFP. Anon (ed.). ACM, p. 112-124 13 p.

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

    5 Scopus citations
  • 1994

    Separate compilation for standard ML

    Appel, A. W. & MacQueen, D. B., Jan 1 1994, Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI). Publ by ACM, p. 13-23 11 p.

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

    2 Scopus citations

  • Space-efficient closure representations

    Shao, Z. & Appel, A. W., 1994, Proceedings of the ACM Conference on LISP and Functional Programming. 3 ed. Publ by ACM, p. 150-161 12 p. (Proceedings of the ACM Conference on LISP and Functional Programming; vol. 7, no. 3).

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

    12 Scopus citations

  • Unrolling lists

    Shao, Z., Reppy, J. H. & Appel, A. W., Jan 1 1994, Proceedings of the ACM Conference on LISP and Functional Programming. 3 ed. Publ by ACM, p. 185-195 11 p. (Proceedings of the ACM Conference on LISP and Functional Programming; vol. 7, no. 3).

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

    26 Scopus citations
  • 1993

    Smartest recompilation

    Shao, Z. & Appel, A. W., 1993, Conference Record of the Annual ACM Symposium on Principles of Programming Languages. Publ by ACM, p. 439-450 12 p. (Conference Record of the Annual ACM Symposium on Principles of Programming Languages).

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

    Open Access
    33 Scopus citations
  • 1991

    Debuggable concurrency extensions for standard ML

    Tolmach, A. P. & Appel, A. W., Dec 1 1991, Proceedings of the 1991 ACM/ONR Workshop on Parallel and Distributed Debugging, PADD 1991. Association for Computing Machinery, Inc, p. 120-131 12 p. (Proceedings of the 1991 ACM/ONR Workshop on Parallel and Distributed Debugging, PADD 1991).

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

  • Standard ML of New Jersey

    Appel, A. W. & MacQueen, D. B., 1991, Programming Language Implementation and Logic Programming - 3rd International Symposium, PLILP 1991, Proceedings. Wirsing, M. & Maluszynski, J. (eds.). Springer Verlag, p. 1-13 13 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 528 LNCS).

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

    126 Scopus citations
  • 1990

    Advisor for flexible working sets

    Alonso, R. & Appel, A. W., 1990, Proc 1990 ACM Sigmetrics Conf Meas Model Comput Syst. Publ by ACM, p. 153-162 10 p. (Proc 1990 ACM Sigmetrics Conf Meas Model Comput Syst).

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

    Open Access
    15 Scopus citations

  • Advisor for flexible working sets

    Alonso, R. & Appel, A. W., Dec 1 1990, 1990 ACM SIGMETRICS Conf Meas Model Comput Syst. Anon (ed.). Publ by ACM, p. 153-162 10 p. (1990 ACM SIGMETRICS Conf Meas Model Comput Syst).

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

    8 Scopus citations

  • Debugging standard ML without reverse engineering

    Tolmach, A. P. & Appel, A. W., 1990, Proc 1990 ACM Conf LISP Funct Program. Publ by ACM, p. 1-12 12 p. (Proc 1990 ACM Conf LISP Funct Program).

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

    6 Scopus citations
  • 1989

    Continuation-passing, closure-passing style

    Appel, A. W. & Jim, T., 1989, Conf Rec Sixteenth Annu ACM Symp Princ Program Lang. Publ by ACM, p. 293-302 10 p. (Conf Rec Sixteenth Annu ACM Symp Princ Program Lang).

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

    34 Scopus citations
  • 1988

    Real-time concurrent collection on stock multiprocessors

    Appel, A. W., Ellis, J. R. & Li, K., Jun 1 1988, Proceedings of the ACM SIGPLAN 1988 Conference on Programming Language Design and Implementation, PLDI 1988. Wexelblat, R. L. (ed.). Association for Computing Machinery, p. 11-20 10 p. (Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI); vol. 20-24-June-1988).

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

    128 Scopus citations
  • 1987

    A standard ML compiler

    Appel, A. W. & MacQueen, D. B., 1987, Functional Programming Languages and Computer Architecture, Proceedings. Kahn, G. (ed.). Springer Verlag, p. 301-324 24 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 274 LNCS).

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

    51 Scopus citations