Andrew W. Appel

Available identifiers

zbMath Open appel.andrew-wWikidataQ4756213 ScholiaQ4756213MaRDI QIDQ1663237

List of research outcomes

Publication	Date of Publication	Type
Verified correctness, accuracy, and convergence of a stationary iterative linear solver: Jacobi method	2024-02-28	Paper
A solver for arrays with concatenation	2023-06-14	Paper
Efficient extensional binary tries	2023-06-14	Paper
Bringing Order to the Separation Logic Jungle	2022-12-09	Paper
Connecting Higher-Order Separation Logic to a First-Order Outside World	2022-10-13	Paper
Abstraction and subsumption in modular verification of C programs	2022-06-20	Paper
C-language floating-point proofs layered with VST and Flocq	2021-12-02	Paper
Corrigendum: C floating-point proofs layered with VST and Flocq	2021-12-02	Paper
VST-Floyd: a separation logic tool to verify correctness of C programs	2018-08-21	Paper
Lambda-splitting	2017-08-21	Paper
Compositional CompCert	2016-09-29	Paper
A theory of indirection via approximation	2015-06-11	Paper
A semantic model of types and machine instructions for proof-carrying code	2015-03-17	Paper
Mostly Sound Type System Improves a Foundational Program Verifier	2015-01-13	Paper
A very modal model of a modern, major, general type system	2014-09-12	Paper
Program Logics for Certified Compilers	2014-07-28	Paper
Verified heap theorem prover by paramodulation	2014-07-21	Paper
Multimodal Separation Logic for Reasoning About Operational Semantics	2014-05-13	Paper
Verified Compilation for Shared-Memory C	2014-04-16	Paper
https://portal.mardi4nfdi.de/entity/Q2871863	2014-01-10	Paper
Efficient Substitution in Hoare Logic Expressions	2013-05-10	Paper
A list-machine benchmark for mechanized metatheory	2013-04-17	Paper
A Certificate Infrastructure for Machine-Checked Proofs of Conditional Information Flow	2012-06-29	Paper
Verified Software Toolchain	2011-05-19	Paper
Formal Verification of Coalescing Graph-Coloring Register Allocation	2010-05-04	Paper
Verification, Model Checking, and Abstract Interpretation	2009-05-15	Paper
Separation Logic for Small-Step cminor	2008-09-02	Paper
Oracle Semantics for Concurrent Separation Logic	2008-04-11	Paper
Verification, Model Checking, and Abstract Interpretation	2007-02-12	Paper
Dependent types ensure partial correctness of theorem provers	2004-09-27	Paper
Polymorphic lemmas and definitions in $\lambda$Prolog and Twelf	2004-09-24	Paper
A trustworthy proof checker	2004-08-06	Paper
Modern Compiler Implementation in Java	2003-06-25	Paper
https://portal.mardi4nfdi.de/entity/Q2723406	2001-07-05	Paper
Shrinking lambda expressions in linear time	1998-08-03	Paper
https://portal.mardi4nfdi.de/entity/Q4379577	1998-03-02	Paper
https://portal.mardi4nfdi.de/entity/Q4343027	1997-06-29	Paper
https://portal.mardi4nfdi.de/entity/Q4343028	1997-06-29	Paper
https://portal.mardi4nfdi.de/entity/Q3026313	1987-01-01	Paper
Generalizations of the sethi‐ullman algorithm for register allocation	1987-01-01	Paper

Research outcomes over time

Doctoral students

No records found.

Known relations from the MaRDI Knowledge Graph

Property	Value
MaRDI profile type	MaRDI person profile
instance of	human

This page was built for person: Andrew W. Appel