PSPL 2010:Keyword Index

Keyword	Papers
A
automata-theoretic decision technique	Tableau-Like Automata-Based Axiomatization for Propositional Linear Temporal Logic
B
Boolean BI	Towards a Cut-free Sequent Calculus for Boolean BI
C
cut elimination	Towards a Cut-free Sequent Calculus for Boolean BI
D
data accessibility	A Multi-Modal Dependent Type Theory for Representing Data Accessibility in a Network
Distributed and Staged Computing	A Multi-Modal Dependent Type Theory for Representing Data Accessibility in a Network
H
Hoare logic	A Developer-oriented Hoare Logic
Hoare-style Logic	A simple proof system for lock-free concurrency
I
Imperative core calculus	A simple proof system for lock-free concurrency
L
lightweight separation	A Developer-oriented Hoare Logic
lock-free algorithms	A simple proof system for lock-free concurrency
M
Modal Type Theory	A Multi-Modal Dependent Type Theory for Representing Data Accessibility in a Network
model checking	Tableau-Like Automata-Based Axiomatization for Propositional Linear Temporal Logic
mu-calculus	A Proof System for Reasoning about Probabilistic Concurrent Processes Tableau-Like Automata-Based Axiomatization for Propositional Linear Temporal Logic
P
Probabilistic concurrent processes	A Proof System for Reasoning about Probabilistic Concurrent Processes
Propositional Linear Temporal Logic	Tableau-Like Automata-Based Axiomatization for Propositional Linear Temporal Logic
S
separation logic	A simple proof system for lock-free concurrency
sequent calculus	Towards a Cut-free Sequent Calculus for Boolean BI
U
understandable verification conditions	A Developer-oriented Hoare Logic