• 3786 Citations
  • 31 h-Index
1985 …2020

Research output per year

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

Research Output

Filter
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 proceedingConference contribution

Open Access

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 proceedingConference contribution

Open Access
2019

Abstraction and subsumption in modular verification of C programs

Beringer, L. & Appel, A. W., Jan 1 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 proceedingConference contribution

1 Scopus citations
2017

Bringing order to the separation logic jungle

Cao, Q., Cuellar, S. & Appel, A. W., Jan 1 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 proceedingConference contribution

2 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 proceedingConference contribution

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 proceedingConference contribution

20 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 proceedingConference contribution

3 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 proceedingConference contribution

30 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 proceedingConference contribution

1 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 proceedingConference contribution

47 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 proceedingConference contribution

8 Scopus citations

Verified compilation for shared-memory C

Beringer, L., Stewart, G., Dockins, R. & Appel, A. W., Jan 1 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 proceedingConference contribution

14 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 proceedingConference contribution

1 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., Apr 9 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 proceedingConference contribution

15 Scopus citations

Verified heap theorem prover by paramodulation

Stewart, G., Beringer, L. & Appel, A. W., Oct 22 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 proceedingConference 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 proceedingConference contribution

2 Scopus citations

Verified software toolchain (Invited talk)

Appel, A. W., Apr 4 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 proceedingConference contribution

65 Scopus citations

VeriSmall: Verified smallfoot shape analysis

Appel, A. W., Nov 28 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 proceedingConference contribution

7 Scopus citations
2010

A logical mix of approximation and separation

Hobor, A., Dockins, R. & Appel, A. W., Dec 1 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 proceedingConference contribution

A theory of indirection via approximation

Hobor, A., Dockins, R. & Appel, A. W., Apr 20 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 proceedingConference contribution

13 Scopus citations

Concurrent separation logic for pipelined parallelization

Bell, C. J., Appel, A. W. & Walker, D., Nov 12 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 proceedingConference contribution

11 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 proceedingConference contribution

67 Scopus citations
2008

Oracle semantics for concurrent separation logic

Hobor, A., Appel, A. W. & Nardelli, F. Z., Jul 21 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 proceedingConference contribution

66 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., Sep 3 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 proceedingConference contribution

44 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 proceedingConference contribution

49 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 proceedingConference contribution

28 Scopus citations
2004

Construction of a semantic model for a typed assembly language

Tan, G., Appel, A. W., Swadi, K. N. & Wu, D., Jan 1 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 proceedingConference contribution

8 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 proceedingConference contribution

8 Scopus citations

Foundational proof-carrying code

Appel, A. W., Jan 1 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 proceedingConference contribution

1 Scopus citations

Foundational Proof Checkers with Small Witnesses

Wu, D., Appel, A. W. & Stump, A., Jan 1 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 proceedingConference contribution

26 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 proceedingConference contribution

Using memory errors to attack a virtual machine

Govindavajhala, S. & Appel, A. W., Jan 1 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 proceedingConference contribution

27 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 proceedingConference contribution

177 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 proceedingConference contribution

17 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 proceedingConference 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 proceedingConference contribution

14 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 proceedingConference contribution

53 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 proceedingConference contribution

25 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 proceedingConference contribution

30 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 proceedingConference contribution

Standard ML of New Jersey

Appel, A. W. & MacQueen, D. B., Jan 1 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 proceedingConference contribution

116 Scopus citations
1990

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 proceedingConference contribution

6 Scopus citations

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 proceedingConference contribution

14 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 proceedingConference contribution

31 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 proceedingConference contribution

74 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 proceedingConference contribution

123 Scopus citations
1987

A standard ML compiler

Appel, A. W. & MacQueen, D. B., Jan 1 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 proceedingConference contribution

43 Scopus citations
1985

SEMANTICS-DIRECTED CODE GENERATION.

Appel, A. W., 1985, Conference Record of the Annual ACM Symposium on Principles of Programming Languages. ACM, p. 315-324 10 p. (Conference Record of the Annual ACM Symposium on Principles of Programming Languages).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

14 Scopus citations