EDBT 2026 Demo / reviewers in the wild / expert
Frances Spalding
dblp:18/151
· DBLP profile ↗
1ranked-venue papers
0as first author
0since 2021 · last 2005
—ORCID · none
Domains — the database's venue-derived domains; a paper can count in several
Theory of computation · 1
Expertise — from the expertise taxonomy: the topics of the expert's papers under the CCF categories. A weight counts papers with recency: 1 for a paper about the topic, 0.3 when the topic is its context, halved every five years.
| Software engineering, system software, and programming languages
1 paper |
Programming languages and type systems · 76% Compilers and program optimization · 19% Runtime systems and virtual machines · 6% |
Topics — the 6 heaviest of 6, each with the papers that count most for it
| Topic | Weight | Papers | Last | Evidence papers |
|---|---|---|---|---|
Programming languages and type systems › type theory
linear logic |
0.1 | 1 | 2005 | Certifying Compilation for a Language with Stack Allocation · LICS 2005 |
Programming languages and type systems › language-based security
memory safety |
0.1 | 1 | 2005 | Certifying Compilation for a Language with Stack Allocation · LICS 2005 |
Programming languages and type systems › type systems › static typing
typed assembly language |
0.1 | 1 | 2005 | Certifying Compilation for a Language with Stack Allocation · LICS 2005 |
Programming languages and type systems
type systems |
0.1 | 1 | 2005 | Certifying Compilation for a Language with Stack Allocation · LICS 2005 |
Compilers and program optimization
verified compilation |
0.1 | 1 | 2005 | Certifying Compilation for a Language with Stack Allocation · LICS 2005 |
Runtime systems and virtual machines › runtime memory management
stack allocation |
0.0 | 1 | 2005 | Certifying Compilation for a Language with Stack Allocation · LICS 2005 |
Methods — techniques the papers use, named apart from their topics
linear logic · 0.1domain-specific predicates · 0.1
| Year | Publication | Venue | Position |
|---|---|---|---|
| 2005 | Certifying Compilation for a Language with Stack AllocationabstractThis paper describes an assembly-language type system capable of ensuring memory safety in the presence of both heap and stack allocation. The type system uses linear logic and a set of domain-specific predicates to specify invariants about the shape of the store. Part of the model for our logic is a tree of "stack tags" that tracks the evolution of the stack over time. To demonstrate the expressiveness of the type system, we define Micro-CLI, a simple imperative language that captures the essence of stack allocation in the common language infrastructure. We show how to compile well-typed Micro-CLI into well-typed assembly. Limin Jia 0001, Frances Spalding, David Walker 0001, Neal Glew |
LICS | 2 |