Theoretical Aspects of Computer Software 4th International Symposium, TACS 2001, Sendai, Japan, October 29-31, 2001. Proceedings /

• Συγγραφή απο Οργανισμό/Αρχή: SpringerLink (Online service)
• Άλλοι συγγραφείς: Kobayashi, Naoki (Επιμελητής έκδοσης, http://id.loc.gov/vocabulary/relators/edt), Pierce, Benjamin C. (Επιμελητής έκδοσης, http://id.loc.gov/vocabulary/relators/edt)
• Μορφή: Ηλεκτρονική πηγή Ηλ. βιβλίο
• Γλώσσα: English
• Έκδοση: Berlin, Heidelberg : Springer Berlin Heidelberg : Imprint: Springer, 2001.
• Έκδοση: 1st ed. 2001.
• Σειρά: Lecture Notes in Computer Science, 2215
• Θέματα: Software engineering.; Application software.; Programming languages (Electronic computers).; Computer logic.; Mathematical logic.; Software Engineering/Programming and Operating Systems.; Computer Applications.; Programming Languages, Compilers, Interpreters.; Logics and Meanings of Programs.; Mathematical Logic and Formal Languages.

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 vol...

Πίνακας περιεχομένων:

• Invited Talk 1
• A Spatial Logic for Concurrency (Part I)
• Session 1
• Boxed Ambients
• A Typed Process Calculus for Fine-Grained Resource Access Control in Distributed Computation
• Formal Eavesdropping and Its Computational Interpretation
• Invited Talk 2
• Resource-Passing Concurrent Programming
• Session 2
• Solo Diagrams
• Observational Equivalence for Synchronized Graph Rewriting with Mobility
• Session 3
• Fixed-Point Logic with the Approximation Modality and Its Kripke Completeness
• Termination Proofs and Complexity Certification
• A Renee Equation for Algorithmic Complexity
• Invited Talk 3
• Nominal Logic: A First Order Theory of Names and Binding
• Session 4
• A Logic Programming Language Based on Binding Algebras
• Proof-Search and Countermodel Generation in Propositional BI Logic
• Generation of a Linear Time Query Processing Algorithm Based on Well-Quasi-Orders
• Invited Talk 4
• Modelisation of Timed Automata in Coq
• Session 5
• Model-Checking LTL with Regular Valuations for Pushdown Systems
• What Will Be Eventually True of Polynomial Hybrid Automata?
• Non-structural Subtype Entailment in Automata Theory
• Session 6
• Bisimulation and Other Undecidable Equivalences for Lossy Channel Systems
• Weakest Congruence Results Concerning "Any-Lock"
• Invited Talk 5
• Design and Correctness of Program Transformations Based on Control-Flow Analysis
• Session 7
• Infinite Intersection and Union Types for the Lazy Lambda Calculus
• Strong Normalization of Second Order Symmetric Lambda-mu Calculus
• The Girard-Reynolds Isomorphism
• Invited Talk 6
• Lightweight Analysis of Object Interactions
• Session 8
• Typing Assembly Programs with Explicit Forwarding
• The UDP Calculus: Rigorous Semantics for Real Networking
• TACS Open Lecture
• Unison: A File Synchronizer and Its Specification.