This volume constitutes the proceedings of the rst IFIP International C- ference on Theoretical Computer Science (IFIP TCS 2000) { Exploring New Frontiers of Theoretical Informatics { organized by IFIP TC1, held at Tohoku University, Sendai, Japan in August 2000.

Breaking and fixing the Needham-Schroeder public-key protocol using FDR.- Reconciling Two Views of Cryptography.- Theory and Construction of Molecular Computers.- Theory and Construction of Molecular Computers.- On the hardness of the permanent.- List Decoding: Algorithms and Applications.- Approximation Algorithms for String Folding Problems.- Approximation Algorithms for String Folding Problems.- Fast multi-dimensional approximate string matching.- An Index for Two Dimensional String Matching Allowing Rotations.- Parallel Edge Coloring of a Tree on a Mesh Connected Computer.- Parallel Edge Coloring of a Tree on a Mesh Connected Computer.- Linear Time 1/2-Approximation Algorithm for Maximum Weighted Matching in General Graphs.- Parallel Approximation Algorithms for Maximum Weighted Matching in General Graphs.- It Is on the Boundary: Complexity Considerations for Polynomial Ideals.- It Is on the Boundary: Complexity Considerations for Polynomial Ideals.- An Efficient Parallel Algorithm for Scheduling Interval Ordered Tasks.- An Efficient Parallel Algorithm for Scheduling Interval Ordered Tasks.- Reducibility among combinatorial problems.- Task Distributions on Multiprocessor Systems.- Fast Interpolation Using Kohonen Self-Organizing Neural Networks.- Fast Interpolation Using Kohonen Self-Organizing Neural Networks.- Steganography Using Modern Arts.- Steganography Using Modern Arts.- Gossiping in Vertex-Disjoint Paths Mode in d-dimensional Grids and Planar Graphs.- Trade-Offs between Density and Robustness in Random Interconnection Graphs.- An effcient way for edge-connectivity augmentation.- The (? + 1)-Edge-Connectivity Augmentation Problem without Creating Multiple Edges of a Graph.- On the Approximability of NP-complete Optimization Problems.- On the Hardness ofApproximating Some NP-Optimization Problems Related to Minimum Linear Ordering Problem.- How Many People Can Hide in a Terrain ?.- Maximum Clique and Minimum Clique Partition in Visibility Graphs.- Language recognition and the synchronization of cellular automata.- Real-Time Language Recognition by Alternating Cellular Automata.- Inducing an order on cellular automata by a grouping operation.- Damage Spreading and ?-Sensitivity on Cellular Automata.- Financial Applications of Monte Carlo and Quasi-Monte Carlo Methods.- Discrepancy Theory and Its Application to Finance.- Fully consistent extensions of partially defined Boolean functions with missing bits.- Fully Consistent Extensions of Partially Defined Boolean Functions with Missing Bitsv.- Dealing necessary and sufficient numbers of cards for sharing a one-bit secret key.- Characterization of Optimal Key Set Protocols.- Algebraic Complexity Theory.- On the Complexity of Integer Programming in the Blum-Shub-Smale Computational Model.- On Logarithmic Simulated Annealing.- On Logarithmic Simulated Annealing.- Specification and verification of concurrent programs in CESAR.- Hierarchical State Machines.- Validating firewalls in mobile ambients.- Ambient Groups and Mobility Types.- Multiway synchronization verified with coupled simulation.- An Asynchronous, Distributed Implementation of Mobile Ambients.- Graph types for monadic mobile processes.- Type Systems for Concurrent Processes: From Deadlock-Freedom to Livelock-Freedom, Time-Boundedness.- Aliasing Models for Mobile Objects.- Local ?-Calculus at Work: Mobile Objects as Mobile Processes.- Typed concurrent objects.- An Interpretation of Typed Concurrent Objects in the Blue Calculus.- Inductive definitions in the system coq. rules and properties.- A Higher-OrderSpecification of the ?-Calculus.- Compositionality through an operational semantics of contexts.- Open Ended Systems, Dynamic Bisimulation and Tile Logic.- Observe behaviour categorically.- Fibred Models of Processes: Discrete, Continuous, and Hybrid Systems.- The Equivalence Problem for Deterministic Pushdown Automata is Decidable.- On the Complexity of Bisimulation Problems for Pushdown Automata.- Session 2.4.- A Type-Theoretic Study on Partial Continuations.- Partially Typed Terms between Church-Style and Curry-Style.- Alternating Automata and Logics over Infinite Words.- Hypothesis Support for Information Integration in Four-Valued Logics.- Invited Talk 2.2.- Masaccio: A Formal Model for Embedded Components.- Session 2.5.- A Single Complete Refinement Rule for Demonic Specifications.- Reasoning about Composition Using Property Transformers and Their Conjugates.- Invited Talk 2.3.- Some New Directions in the Syntax and Semantics of Formal Languages.- Panel Discussion on New Challanges for TCS.- New Challenges for Theoretical Computer Science.- Algorithm Design Challenges.- Quantumization of Theoretical Informatics.- Two Problems in Wide Area Network Programming.- New Challenges for Computational Models.- Towards a Computational Theory of Everything.- Open Lectures.- On the Power of Interactive Computing.- The Varieties of Programming Language Semantics.