• 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
Article
2018

VST-Floyd: A Separation Logic Tool to Verify Correctness of C Programs

Cao, Q., Beringer, L., Gruetter, S., Dodds, J. & Appel, A. W., Jun 1 2018, In : Journal of Automated Reasoning. 61, 1-4, p. 367-422 56 p.

Research output: Contribution to journalArticle

16 Scopus citations
2017

Position paper: the science of deep specification

Appel, A. W., Beringer, L., Chlipala, A., Pierce, B. C., Shao, Z., Weirich, S. & Zdancewic, S., Oct 13 2017, In : Philosophical Transactions of the Royal Society A: Mathematical, Physical and Engineering Sciences. 375, 2104, 20160331.

Research output: Contribution to journalArticle

10 Scopus citations
2015

Compositional CompCert

Stewart, G., Beringer, L., Cuellar, S. & Appel, A. W., Jan 2015, In : ACM SIGPLAN Notices. 50, 1, p. 275-287 13 p.

Research output: Contribution to journalArticle

4 Scopus citations

Verification of a cryptographic primitive: SHA-256 7

Appel, A. W., Apr 1 2015, In : ACM Transactions on Programming Languages and Systems. 37, 2, 7.

Research output: Contribution to journalArticle

53 Scopus citations
2012

A list-machine benchmark for mechanized metatheory

Appel, A. W., Dockins, R. & Leroy, X., Oct 1 2012, In : Journal of Automated Reasoning. 49, 3, p. 453-491 39 p.

Research output: Contribution to journalArticle

4 Scopus citations

Creating and preserving locality of Java applications at allocation and garbage collection times

Shuf, Y., Gupta, M., Franke, H., Appel, A. W. & Singh, J. P., Nov 2012, In : ACM SIGPLAN Notices. 37, 11, p. 13-25 13 p.

Research output: Contribution to journalArticle

Verified heap theorem prover by paramodulation

Stewart, G., Beringer, L. & Appel, A. W., Sep 1 2012, In : ACM SIGPLAN Notices. 47, 9, p. 3-14 12 p.

Research output: Contribution to journalArticle

1 Scopus citations
2011

Security seals on voting machines: A case study

Appel, A. W., Sep 2011, In : ACM Transactions on Information and System Security. 14, 2, 18.

Research output: Contribution to journalArticle

10 Scopus citations
2010

A theory of indirection via approximation

Hobor, A., Dockinsy, R. & Appel, A. W., Jan 2010, In : ACM SIGPLAN Notices. 45, 1, p. 171-184 14 p.

Research output: Contribution to journalArticle

6 Scopus citations

Semantic foundations for typed assembly languages

Ahmed, A., Appel, A. W., Richards, C. D., Swadi, K. N., Tan, G. & Wang, D. C., Mar 1 2010, In : ACM Transactions on Programming Languages and Systems. 32, 3, 1709094.

Research output: Contribution to journalArticle

14 Scopus citations
2008

Multimodal Separation Logic for Reasoning About Operational Semantics

Dockins, R., Appel, A. W. & Hobor, A., Oct 22 2008, In : Electronic Notes in Theoretical Computer Science. 218, C, p. 5-20 16 p.

Research output: Contribution to journalArticle

5 Scopus citations
2007

A List-machine Benchmark for Mechanized Metatheory. (Extended Abstract)

Appel, A. W. & Leroy, X., Jun 2 2007, In : Electronic Notes in Theoretical Computer Science. 174, 5, p. 95-108 14 p.

Research output: Contribution to journalArticle

4 Scopus citations

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

Appel, A. W., Melliès, P. A., Richards, C. D. & Vouillon, J., Jan 2007, In : ACM SIGPLAN Notices. 42, 1, p. 109-122 14 p.

Research output: Contribution to journalArticle

25 Scopus citations
2004

Dependent types ensure partial correctness of theorem provers

Appel, A. W. & Felty, A. P., Jan 1 2004, In : Journal of Functional Programming. 14, 1, p. 3-19 17 p.

Research output: Contribution to journalArticle

14 Scopus citations

Polymorphic lemmas and definitions in λProlog and Twelf

Appel, A. W. & Felty, A. P., Jan 1 2004, In : Theory and Practice of Logic Programming. 4, 1-2, p. 1-39 39 p.

Research output: Contribution to journalArticle

3 Scopus citations

Real-time concurrent collection on stock multiprocessors

Appel, A. W., Apr 1 2004, In : ACM SIGPLAN Notices. 39, 4, p. 205-206 2 p.

Research output: Contribution to journalArticle

1 Scopus citations

Real-time concurrent collection on stock multiprocessors

Appel, A. W., Ellis, J. R. & Li, K., Apr 1 2004, In : ACM SIGPLAN Notices. 39, 4, p. 207-216 10 p.

Research output: Contribution to journalArticle

1 Scopus citations
2003

A Trustworthy Proof Checker

Appel, A. W., Michael, N., Stump, A. & Virga, R., 2003, In : Journal of Automated Reasoning. 31, 3-4, p. 231-260 30 p.

Research output: Contribution to journalArticle

18 Scopus citations

Mechanisms for secure modular programming in Java

Bauer, L., Appel, A. W. & Felten, E. W., Apr 25 2003, In : Software - Practice and Experience. 33, 5, p. 461-480 20 p.

Research output: Contribution to journalArticle

14 Scopus citations
2001

An indexed model of recursive types for foundational proof-carrying code

Appel, A. W. & McAllester, D., Sep 1 2001, In : ACM Transactions on Programming Languages and Systems. 23, 5, p. 657-683 27 p.

Research output: Contribution to journalArticle

168 Scopus citations

Optimal spilling for CISC machines with few registers

Appel, A. W. & George, L., May 2001, In : SIGPLAN Notices (ACM Special Interest Group on Programming Languages). 36, 5, p. 243-253 11 p.

Research output: Contribution to journalArticle

8 Scopus citations

Type-preserving garbage collectors

Wang, D. C. & Appel, A. W., Jan 1 2001, In : SIGPLAN Notices (ACM Special Interest Group on Programming Languages). 36, 3, p. 166-178 13 p.

Research output: Contribution to journalArticle

9 Scopus citations
2000

Efficient and safe-for-space closure conversion

Shao, Z. & Appel, A. W., Jan 2000, In : ACM Transactions on Programming Languages and Systems. 22, 1, p. 129-161 33 p.

Research output: Contribution to journalArticle

12 Scopus citations

SAFKASI: A security mechanism for language-based systems

Wallach, D. S., Appel, A. W. & Felten, E. W., Oct 2000, In : ACM Transactions on Software Engineering and Methodology. 9, 4, p. 341-378 38 p.

Research output: Contribution to journalArticle

87 Scopus citations
1999

Hierarchical modularity

Blume, M. & Appel, A. W., Jul 1999, In : ACM Transactions on Programming Languages and Systems. 21, 4, p. 813-847 35 p.

Research output: Contribution to journalArticle

41 Scopus citations
1998

SSA is Functional Programming

Appel, A. W., Apr 1998, In : SIGPLAN Notices (ACM Special Interest Group on Programming Languages). 33, 4, p. 17-20 4 p.

Research output: Contribution to journalArticle

99 Scopus citations
1997

Lambda-Splitting: A Higher-Order Approach to Cross-Module Optimizations

Blume, M. & Appel, A. W., Jan 1 1997, In : SIGPLAN Notices (ACM Special Interest Group on Programming Languages). 32, 8, p. 112-124 13 p.

Research output: Contribution to journalArticle

3 Scopus citations

Shrinking lambda expressions in linear time

Appel, A. W. & Jim, T., Sep 1997, In : Journal of Functional Programming. 7, 5, p. 515-540 26 p.

Research output: Contribution to journalArticle

32 Scopus citations
1996

Empirical and analytic study of stack versus heap cost for languages with closures

Appel, A. W. & Shao, Z., Jan 1996, In : Journal of Functional Programming. 6, 1, p. 47-74 28 p.

Research output: Contribution to journalArticle

17 Scopus citations

Intensional Equality ;= for Continuations

Appel, A. W., Feb 1996, In : SIGPLAN Notices (ACM Special Interest Group on Programming Languages). 31, 2, p. 55-57 3 p.

Research output: Contribution to journalArticle

3 Scopus citations

Iterated Register Coalescing

George, L. & Appel, A. W., May 1996, In : ACM Transactions on Programming Languages and Systems. 18, 3, p. 300-324 25 p.

Research output: Contribution to journalArticle

178 Scopus citations
1995

A Debugger for standard ML

Tolmhch, A. & Appel, A. W., Apr 1995, In : Journal of Functional Programming. 5, 2, p. 155-200 46 p.

Research output: Contribution to journalArticle

30 Scopus citations

A Type-Based Compiler for Standard ML

Shao, Z. & Appel, A. W., Jan 6 1995, In : ACM SIGPLAN Notices. 30, 6, p. 116-129 14 p.

Research output: Contribution to journalArticle

53 Scopus citations
1994

Axiomatic Bootstrapping: A Guide for Compiler Hackers

Appel, A. W., Jan 11 1994, In : ACM Transactions on Programming Languages and Systems (TOPLAS). 16, 6, p. 1699-1718 20 p.

Research output: Contribution to journalArticle

6 Scopus citations

Loop headers in λ-calculus or CPS

Appel, A. W., Dec 1 1994, In : LISP and Symbolic Computation. 7, 4, p. 337-343 7 p.

Research output: Contribution to journalArticle

7 Scopus citations

Separate compilation for standard ml

Appel, A. W. & MacQueen, D. B., Jan 6 1994, In : ACM SIGPLAN Notices. 29, 6, p. 13-23 11 p.

Research output: Contribution to journalArticle

1 Scopus citations
1993

A critique of Standard ML

Appel, A. W., Oct 1993, In : Journal of Functional Programming. 3, 4, p. 391-429 39 p.

Research output: Contribution to journalArticle

8 Scopus citations

Special Issue on ML

Appel, A. W. & Harper, R., Jan 1 1993, In : Journal of Functional Programming. 3, 4, 1 p.

Research output: Contribution to journalArticle

1992

Callee-save registers in continuation-passing style

Appel, A. W. & Shao, Z., Sep 1 1992, In : LISP and Symbolic Computation. 5, 3, p. 191-221 31 p.

Research output: Contribution to journalArticle

12 Scopus citations

Is POPL Mathematics or Science?

Appel, A. W., Jan 4 1992, In : ACM SIGPLAN Notices. 27, 4, p. 87-89 3 p.

Research output: Contribution to journalArticle

1 Scopus citations

Special Issue On Ml

Appel, A. W. & Harper, R., Jan 1 1992, In : Journal of Functional Programming. 2, 1, p. i

Research output: Contribution to journalArticle

1991

Debuggable concurrency extensions for standard ML

Tolmach, A. P. & Appel, A. W., Jan 12 1991, In : ACM SIGPLAN Notices. 26, 12, p. 120-131 12 p.

Research output: Contribution to journalArticle

10 Scopus citations

Virtual memory primitives for user programs

Appel, A. W. & Li, K., Jan 4 1991, In : ACM SIGPLAN Notices. 26, 4, p. 96-107 12 p.

Research output: Contribution to journalArticle

29 Scopus citations
1990

A runtime system

Appel, A. W., Nov 1 1990, In : Lisp and Symbolic Computation. 3, 4, p. 343-380 38 p.

Research output: Contribution to journalArticle

27 Scopus citations
1989

Allocation without locking

Appel, A. W., Jul 1989, In : Software: Practice and Experience. 19, 7, p. 703-705 3 p.

Research output: Contribution to journalArticle

6 Scopus citations

Runtime tags aren't necessary

Appel, A. W., Jun 1 1989, In : Lisp and Symbolic Computation. 2, 2, p. 153-162 10 p.

Research output: Contribution to journalArticle

29 Scopus citations

Simple generational garbage collection and fast allocation

Appel, A. W., Feb 1989, In : Software: Practice and Experience. 19, 2, p. 171-183 13 p.

Research output: Contribution to journalArticle

184 Scopus citations

Vectorized garbage collection

Appel, A. W. & Bendiksen, A., Sep 1 1989, In : The Journal of Supercomputing. 3, 3, p. 151-160 10 p.

Research output: Contribution to journalArticle

5 Scopus citations
1988

Real-time Concurrent Collection on Stock Multiprocessors

Appel, A. W., Ellis, J. R. & Li, K., Jul 1 1988, In : ACM SIGPLAN Notices. 23, 7, p. 11-20 10 p.

Research output: Contribution to journalArticle

18 Scopus citations
13 Scopus citations