Programming Languages and Systems Book

	A Query Language Based on the Ambient Logic	1
	Probabilistic Polynomial-Time Process Calculus and Security Protocol Analysis	23
	A Systematic Approach to Static Access Control	30
	Secure Information Flow and CPS	46
	Enforcing Safety Properties Using Type Specialization	62
	Semantics and Program Analysis of Computationally Secure Information Flow	77
	Encoding Intensional Type Analysis	92
	Fusion on Languages	107
	Programming the Web with High-Level Programming Languages	122
	On the Completeness of Model Checking	137
	Modal Transition Systems: A Foundation for Three-Valued Program Analysis	155
	Entailment with Conditional Equality Constraints	170
	On the Complexity of Constant Propagation	190
	What Are Polymorphically-Typed Ambients?	206
	JOIN (X): Constraint-Based Type Inference for the Join-Calculus	221
	Modular Causality in a Synchronous Stream Language	237
	Control-Flow Analysis in Cubic Time	252
	The Recursive Record Semantics of Objects Revisited	269
	A Formalisation of Java's Exception Mechanism	284
	A Formal Executable Semantics of the JavaCard Platform	302
	Modeling an Algebraic Stepper	320
	Typestate Checking of Machine Code	335
	Proof-Directed De-compilation of Low-Level Code	352
	Backwards Abstract Interpretation of Probabilistic Programs	367
	Tool Demonstration: Finding Duplicated Code Using Program Dependences	383
	Compiling Problem Specification into SAT	387
	Semantics and Termination of Simply-Moded Logic Programs with Dynamic Scheduling	402
	The Def-inite Approach to Dependency Analysis	417
	Author Index	433