Theoretical Aspects of Computer Software: 4th International Symposium, TACS 2001, Sendai, Japan, October 29-31, 2001. Proceedings (Lecture Notes in Computer Science)

This volume constitutes the proceedings of the Fourth International Symposium on Theoretical Aspects of Computer Software (TACS 2001) held at Tohoku U- versity, Sendai, Japan in October 2001. The TACS symposium focuses on the theoretical foundations of progr- ming and their applications. As this volume shows, TACS is an international symposium, with participants from many di?erent institutions and countries. TACS 2001 was the fourth symposium in the TACS series, following TACS’91, TACS’94, and TACS’97, whose proceedings were published as Volumes 526, 789, and 1281, respectively, of Springer-Verlag’s Lecture Notes in Computer Science series. The TACS 2001 technical program consisted of invited talks and contributed talks. In conjunction with this program there was a special open lecture by Benjamin Pierce; this lecture was open to non-registrants. TACS 2001 bene?ted from the e?orts of many people; in particular, members of the Program Committee and the Organizing Committee. Our special thanks go to the Program Committee Co-chairs: Naoki Kobayashi (Tokyo Institute of Technology) Benjamin Pierce (University of Pennsylvania). Theoretical Aspects of Computer Software Foreword Preface Program Committee Additional Referees Table of Contents A Spatial Logic for Concurrency 1 Introduction 2 Preliminaries on the Asynchronous π-Calculus 3 Syntax of the Spatial Logic 4 Semantics 4.1 Property Sets 4.2 Satisfaction 4.3 Discussion 5 Validity 6 Fresh and Hidden Name Quantification 6.1 The Fresh Name Quantifier 6.2 The Hidden Name Quantifier 7 Recursive De .nitions 8 Conclusions References Appendix Boxed Ambients 1 Introduction 1.1 Mobile Ambients 1.2 Boxed Ambients: Overview and Main Results 1.3 Plan of the Paper 2 Boxed Ambients 3 Communication Channels 3.1 π-Calculus Channels 3.2 Parent-Child Channeled Communication à la Seal Calculus 4 Typing Boxed Ambients 4.1 Types 4.2 Typing Rules 5 Mobile Ambients versus Boxed Ambients 5.1 Security and Resource Access Control 5.2 Discussion 6 Moded Typing 6.1 Moded Types 6.2 Capabilities and Moded Judgments 6.3 Typing Rules 6.4 Subject Reduction 7 Asynchronous Communications 7.1 Synchrony versus Asynchrony: Security Trade-Offs 8 Conclusion and Related Work References A Moded Typing: The Complete Type System A Typed Process Calculus for Fine-Grained Resource Access Control in Distributed Computation 1 Introduction 2 The Language 2.1 Syntax 2.2 Operational Semantics 2.3 Example 3 The Type System 3.1 Environments and Partially Ordered Sets of Domains 3.2 Typing Rules 4 Type Soundness 4.1 Subject Reduction 4.2 The Tagged Language and Type Safety 5 Subtyping 6 Related Work 7 Future Work Acknowledgment References Formal Eavesdropping and Its Computational Interpretation 1 Introduction 2 The Language (Syntax and Informal Semantics) 3 Formal Model 4 Computational Model 5 Soundness 6 Conclusion Acknowledgements References Resource-Passing Concurrent Programming 1 Introduction - Constraint-Based Concurrency 2 The Essence of Constraint-Based Communication 2.1 The Language 2.2 Operational Semantics 2.3 Relation to Name-Based Concurrency 2.4 Locality in Global Store 3 I/O Mode Analysis 3.1 Motivation 3.2 The Mode System 3.3 Mode Analysis 3.4 Moding Principles 3.5 Properties of Well-Moded Programs 3.6 Mode Graphs and Principal Modes 4 Linearity Analysis 4.1 Motivation and Observation 4.2 The Linearity System 5 From Linearity to Strict Linearity 5.1 Polarizing Constructors 5.2 Strict Linearity 5.3 Void: The Zero-Capability Symbol 5.4 Constant-Time Property of Strictly Linear Programs 6 Allowing Concurrent Access within Strict Linearity 7 Operational Semantics with Capability Counting 8 The Capability System 9 Related Work 10 Conclusions and Future Work Acknowledgments References Solo Diagrams 1 Introduction 2 The Solos Calculus 2.1 The Implementation of the Replication Operator 3 Solo Diagrams 3.1 A Local Implementation of Boxes 3.2 The Connection with Proof Nets 4 Agents and Solo Diagrams 5 Multi-labelled Solo Diagrams 6 Related Work References Observational Equivalence for Synchronized Graph Rewriting with Mobility 1 Introduction 2 Synchronized Graph Rewriting with Mobility 3 Representation of Graphs in a P-Monoidal Category 4 A Tile Logic Representation for Synchronized Graph Rewriting with Mobility 5 Bisimilarity Is a Congruence 6 Bisimulation Up-to Congruence 7 Example: Communication Network 8 Conclusion Acknowledgements References Fixed-Point Logic with the Approximation Modality and Its Kripke Completeness 1 Introduction 2 The Typing Systems 3 Semantics 4 The Modal Logic behind S-λ•μ and F-λ•μ 5 Relationship to the Intuitionistic Logic of Provability 6 Concluding Remarks References Appendix:Proof of Theorem 2 Termination Proofs and Complexity Certification 1 Introduction 1.1 Main Results 1.2 Motivation and Benefits 1.3 Comparisons 2 The Methodology of Intrinsic Theories 2.1 Intrinsic Theories 2.2 Provable Functions 2.3 The Generic Setting 3 Statement of the Results 3.1 Data-Positive Induction and Primitive Recursion 3.2 Data-Predicative Derivations 3.3 Classical vs. Constructive Logic 3.4 Relativized Results 4 From Computational Complexity to Provability 5 From Provability to Computational Complexity 5.1 Typed Lambda Calculus with Recurrence 5.2 Natural Deduction Derivations as Applicative Programs 5.3 Function Provability and Recurrence in Higher Type 5.4 Complexity from Provability References A Renee Equation for Algorithmic Complexity 1 Introduction 2 Background 2.1 Domain Theory 2.2 Examples of Domains 2.3 The μTopology 2.4 The Renee Equation 2.5 The Recursive Functions 3 Verification 4 Complexity 5 An Analysis of Search Methods 6 Conclusion References Nominal Logic: A First Order Theory of Names and Binding 1 Introduction 2 Equivariant Predicates 3 Nominal Logic: Syntax and Semantics 4 Nominal Logic Axioms 5 The Freshness Quantifier 6 Binding 7 Choice 8 Related Work References A Logic Programming Language Based on Binding Algebras 1 Introduction 2 Terms 3 Object Variable Substitutions 4 Type System and Its Interpretation 5 Free Object Variable Substitutions 6 Substitutions on Terms 7 Equational Logic 8 Unification 9 Binding Logic Programming 9.1 Logic 9.2 Operational Semantics 10 Related Work References Proof-Search and Countermodel Generation in Propositional BI Logic 1 Introduction 2 The Logic of Bunched Implications (BI) 2.1 Syntax and Proof-Theory of BI 2.2 Kripke Resource Semantics 2.3 Resources and Sharing Interpretation 3 A Labelled Tableaux Calculus for BI^+ 3.1 A Labelling Algebra 3.2 Labelled Formulae and Configurations 3.3 An Example 4 Properties of the TBI Calculus 4.1 Soundness 4.2 A Tableau Construction Procedure 4.3 Countermodel Construction 4.4 Completeness and Finite Model Property 4.5 Extraction of a Countermodel 5 Conclusion References A Proof of Lemma 3 B Proof of Theorem 9 Generation of a Linear Time Query Processing Algorithm Based on Well-Quasi-Orders 1 Introduction 2 A Tour 3 Disjunctive Monadic Query on Indefinite Database 4 Higman's Lemma and the Constructive Proof 4.1 Constructive Proof by Murthy-Russell 4.2 An Extension 5 Algorithm Generation Based on WQO Techniques 5.1 Design of Disjunctive Query Processing Algorithm 5.2 Construction of ExistsMinor(L) 6 Concluding Remarks Acknowledgments References Modelisation of Timed Automata in Coq 1 Introduction 1.1 Theorem Proving vs Model-Checking 1.2 Studying a Conformance Protocol 1.3 Outline of the Paper 2 Description of Coq 2.1 What Is Coq? 2.2 Particularities of Coq 2.3 Notations 3 Description of p-Automata 4 Encoding p-Automata in Coq 4.1 Deep versus Shallow Embeddings 4.2 The Type of p-Automata 4.3 Semantics 4.4 Synchronization 4.5 Representing a Specific Automata 5 Automation of Proofs 6 Conclusion Acknowledgements References Model-Checking LTL with Regular Valuations for Pushdown Systems 1 Introduction 2 Preliminaries 2.1 Transition Systems 2.2 The Logic LTL 2.3 Pushdown Systems 3 LTL on Pushdown Systems 3.1 Model-Checking with Regular Valuations 4 Applications 4.1 Interprocedural Data-Flow Analysis 4.2 Pushdown Systems with Checkpoints 4.3 Model-Checking CTL* 5 Lower Bounds 6 Conclusion References What Will Be Eventually True of Polynomial Hybrid Automata? 1 Introduction 2 Hybrid Automata 3 Progress Properties and State Recurrence 3.1 A Simple Model of Noise 3.2 Infinite Pathsand Noisy State Recurrence 4 An Automatic Verification Procedure for Progress 5 Decidability of Robustness 6 Discussion Acknowledgements References Non-structural Subtype Entailment in Automata Theory 1 Introduction 2 Characterization 3 Non-structural Subtype Constraints 3.1 Non-structural Subtyping 3.2 Constraint Language 4 Entailment via Safety 5 Cap Automata and Cap Sets 6 Automata Construction 7 Soundness 8 Completeness 9 Restrictions of Constructed Automata 10 Restricted Cap Set Expressions 11 Back Translation for Restricted Cap Automata 12 Equivalence of Variants of NSSE Conclusion and Future Work Acknowledgements References Bisimulation and Other Undecidable Equivalences for Lossy Channel Systems 1 Introduction 2 Basic Notions 2.1 Words and the Subword Relation 2.2 Labeled Transition Systems and Behavioral Equivalences 3 Channel Systems 3.1 Standard Channel Systems and Other Restrictions 3.2 Undecidability of Reachability 3.3 Lossy Channel Systems 4 Reducing from Perfect to Lossy Systems 5 Classic-Lossy Systems with One Channel 6 Conclusion A Technical Appendix A.1 Proof of Lemma 4.1 A.2 Proof of Lemma 4.2 References Weakest Congruence Results Concerning "Any-Lock" 1 Introduction 2 Background 3 The Weakest Any-Lock-Preserving Congruence 4 The Weakest Any-Lock-Trace-Preserving Congruence 5 Weakest Congruence Characterisation of CSP-Equivalence 6 Related Work 7 Conclusions Acknowledgements References Design and Correctness of Program Transformations Based on Control-Flow Analysis 1 Introduction 2 The Source Language 3 The Target Language 4 Defunctionalization 5 Flow-Based Inlining 6 Lightweight Defunctionalization 7 Discussion Acknowledgements References A Imperative Features A.1 The Source Language A.2 The Target Language A.3 Translation into Target Infinite Intersection and Union Types for the Lazy Lambda Calculus 1 Introduction 2 The Lazy Lambda Calculus 3 An Infinitary Type Theory 4 The Type Assignment System 5 Conclusion References Strong Normalization of Second Order Symmetric Lambda-mu Calculus 1 Introduction 2 Symmetric λ μ-calculus 3 Extraction of Witnesses from Σ 0 -formulae 4 Strong Normalization Acknowledgement References The Girard-Reynolds Isomorphism 1 Introduction 2 Second-Order Lambda Calculus and Logic 3 The Reynolds Embedding and the Girard Projection 4 Doubling and Parametricity 5 Algebraic Types and Parametricity 5.1 Every Algebraic Type is Extensive 5.2 Every Algebraic Type is Deductive 5.3 Inductive Implies Parametric 5.4 Parametric Implies Inductive Acknowledgements References Lightweight Analysis of Object Interactions 1 Motivations 2 Example 3 An Approach 3.1 A Relational Heap Model 3.1.1 Generic Heap Structure 3.1.2 Abstract Specifications of Classes 3.1.3 Extracted Specifications of Classes 3.2 Declarative Specification 3.2.1 Linking Objects 3.2.2 Non-determinism 3.2.3 Mutation at a Distance 3.2.4 Comodification 3.2.5 Subtypes and Subclasses 3.3 Extraction and Constraint Solving 3.3.1 Checking Comodification 3.3.2 Extending the Correctness Argument 3.3.3 Issues. 4 Related Work 4.1 Object Interaction 4.2 Interface Specification Languages 4.3 Model Extraction 4.4 Static Analysis Acknowledgments References Typing Assembly Programs with Explicit Forwarding 1 Introduction 1.1 Related Work 2 Assembly Language and Sequential Execution 2.1 Syntax and Operational Model 2.2 Type System 3 Distributed Execution 3.1 Operational Model 3.2 A Type System for Deterministic Execution 3.3 Finite Operand Queues 4 Program Execution 4.1 Sequential Execution 4.2 Distributed Execution 5 Discussion Acknowledgements References The UDP Calculus: Rigorous Semantics for Real Networking 1 Introduction 1.1 Background and Problem 1.2 Contribution 1.3 Experimental Semantics 1.4 Overview 1.5 Background: Networks and Protocols, Informally 1.6 Background: The Sockets Interface, Informally 1.7 Choices: What to Model? 1.8 Structuring the Model (and Language Independence) 1.9 It's Not Really So Easy 2 UDP - The Model 2.1 Statics: Types, Values, and Judgements 2.1.1 Hosts and Threads 2.1.2 Sockets 2.1.3 The Sockets Interface 2.1.4 Networks 2.2 Dynamics: Interaction 2.2.1 Thread LTSs and Language Independence 2.2.2 Network Operational Semantics 2.3 Highlights of the Host Semantics 2.3.1 Ports 2.3.2 Message Delivery to the Net 2.3.3 Return From a Fast Call 2.3.4 Message Delivery from the Net 2.3.5 ICMP Generation 2.3.6 Asynchronous Errors 2.3.7 Local Errors 2.3.8 Loopback 2.4 Sanity Properties 3 MiniCaml 4 Validation 5 Examples 5.1 The Single Sender 5.2 The Single Heartbeat 6 Related Work 7 Conclusion Acknowledgements References Unison: A File Synchronizer and Its Specification Author Index This book constitutes the refereed proceedings of the Fourth International Symposium on Theoretical Aspects of Computer Software, TACS 2001, held in Sendai, Japan, in October 2001. The book presents 21 selected and revised full papers. Also included are six invited papers plus one open lecture by internationally leading scientists. Among the topics addressed are automata theory, concurrency, control-flow analysis, lambda calculi, model checking and program logic