Frances Spalding

dblp:18/151 · DBLP profile ↗
← Back
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

TopicWeightPapersLastEvidence papers
Programming languages and type systems › type theory
linear logic
0.112005
Certifying Compilation for a Language with Stack Allocation · LICS 2005
Programming languages and type systems › language-based security
memory safety
0.112005
Certifying Compilation for a Language with Stack Allocation · LICS 2005
Programming languages and type systems › type systems › static typing
typed assembly language
0.112005
Certifying Compilation for a Language with Stack Allocation · LICS 2005
Programming languages and type systems
type systems
0.112005
Certifying Compilation for a Language with Stack Allocation · LICS 2005
Compilers and program optimization
verified compilation
0.112005
Certifying Compilation for a Language with Stack Allocation · LICS 2005
Runtime systems and virtual machines › runtime memory management
stack allocation
0.012005
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
YearPublicationVenuePosition
2005 Certifying Compilation for a Language with Stack Allocation
abstract
This 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
LICS2