Foundations of Software Science and Computation Structures Book

	Adequacy for Algebraic Effects	1
	Secrecy Types for Asymmetric Communication	25
	Axiomatizing Tropical Semirings	42
	Type Isomorphisms and Proof Reuse in Dependent Type Theory	57
	On the Duality between Observability and Reachability	72
	The Finite Graph Problem for Two-Way Alternating Automata	88
	High-Level Petri Nets as Type Theories in the Join Calculus	104
	Temporary Data in Shared Dataspace Coordination Languages	121
	On Garbage and Program Logic	137
	The Complexity of Model Checking Mobile Ambients	152
	The Rho Cube	168
	Type Inference with Recursive Type Equations	184
	On the Modularity of Deciding Call-by-Need	199
	Synchronized Tree Languages Revisited and New Applications	214
	Computational Completeness of Programming Languages Based on Graph Transformation	230
	Axioms for Recursion in Call-by-Value	246
	Class Analysis of Object-Oriented Programs through Abstract Interpretation	261
	On the Complexity of Parity Word Automata	276
	Foundations for a Graph-Based Approach to the Specification of Access Control Policies	287
	Categories of Processes Enriched in Final Coalgebras	303
	Model Checking CTL[superscript +] and FCTL Is Hard	318
	On Regular Message Sequence Chart Languages and Relationships to Mazurkiewicz Trace Theory	332
	Verified Bytecode Verifiers	347
	Higher-Order Abstract Syntax with Induction in Isabelle/HOL: Formalizing the [pi]-Calculus and Mechanizing the Theory of Contexts	364
	Decidability of Weak Bisimilarity for a Subset of Basic Parallel Processes	379
	An Axiomatic Semantics for the Synchronous Language Gentzen	394
	Marrella and the Verification of an Embedded System	409
	Author Index	413