close
1.

図書

図書
sponsored by IEEE Computer Society Technical Committee on Mathematical Foundations of Computing
出版情報: Los Alamitos, Calif. ; Tokyo : IEEE Computer Society, c2001  xii, 441 p. ; 28 cm
所蔵情報: loading…
2.

図書

図書
sponsored by IEEE Computer Society Technical Committee on Mathematical Foundations of Computing ; with support from Forall Systems IBM
出版情報: Los Alamitos, Calif. ; Tokyo : IEEE Computer Society, c2005  xiii, 477 p. ; 28 cm
所蔵情報: loading…
3.

図書

図書
sponsored by IEEE Technical Committee on Mathematical Foundations of Computing ; with support from Academy of Finland ... [et al.]
出版情報: Los Alamitos, Calif. ; Tokyo : IEEE Computer Society, c2004  xiii, 467 p. ; 28 cm
所蔵情報: loading…
4.

図書

図書
sponsored by IEEE Computer Society Technical Committee on Mathematical Foundations of Computing ; in cooperation with Association for Symbolic Logic, European Association for Theoretical Computer Science ; with support from Fields Institute for Research in Mathematical Sciences, Le Centre de Recherches Mathématiques (CRM), University of Ottawa
出版情報: Los Alamitos, Calif. ; Tokyo : IEEE Computer Society, c2003  xiv, 393 p. ; 28 cm
所蔵情報: loading…
目次情報: 続きを見る
Foreword
Conference Organization
Program Committee
Additional Reviewers
Proof Nets for Unit-Free Multiplicative-Additive Linear Logic / D. Hughes ; R. van GlabbeekSession 1:
About Translations of Classical Logic into Polarized Linear Logic / O. Laurent ; L. Regnier
System ST [beta]-Reduction and Completeness / C. Raffalli
Invited Tutorial--Types and Programming Languages: The Next Generation / B. C. PierceSession 2:
Reasoning about Hierarchical Storage / A. Ahmed ; L. Jia ; D. WalkerSession 3:
Invited Talk--Formal Verification at Intel / J. Harrison
New Directions in Instantiation-Based Theorem Proving / H. Ganzinger ; K. KorovinSession 4:
Abstract Saturation-Based Inference / N. Dershowitz ; C. Kirchner
Orienting Equalities with the Knuth-Bendix Order / A. Voronkov
Practical Reflection in Nuprl / E. Barzilay ; S. Allen ; R. ConstableShort Presentations I:
An Applicative-Order Term Rewriting System for Code Generation, and Its Termination Analysis / O. Kiselyov
Patterns Based on Multiple Interacting Partial Orders / F. J. Oles
Logic of Subtyping / P. Naumov
A Language and a Notion of Truth for Cryptographic Properties / S. Kramer
The Relative Complexity of Local Search Heuristics and the Iteration Principle / T. Morioka
A Second-Order Theory for NL / S. Cook ; A. Kolokolova
Dependent Intersection: A New Way of Defining Records in Type Theory / A. KopylovSession 5:
Structural Subtyping of Non-Recursive Types Is Decidable / V. Kuncak ; M. Rinard
On Program Equivalence in Languages with Ground-Type References / A. S. Murawski
A Proof Theory for Generic Judgments: An Extended Abstract / D. Miller ; A. TiuSession 6:
Polynomial-Time Algorithms from Ineffective Proofs / P. Oliva
The Complexity of Resolution Refinements / J. Buresh-Oppenheim ; T. Pitassi
Successor-Invariance in the Finite / B. RossmanSession 7:
Invited Talk--Will Deflation Lead to Depletion? On Non-Monotone Fixed Point Inductions / E. Gradel ; S. Kreutzer
On Automatic Partial Orders / B. Khoussainov ; S. Rubin ; F. StephanSession 8:
Logical Definability and Query Languages over Unranked Trees / L. Libkin ; F. Neven
Query Evaluation on Compressed Trees / M. Frick ; M. Grohe ; C. Koch
Revisiting Digitization, Robustness, and Decidability for Timed Automata / J. Ouaknine ; J. WorrellSession 9:
Satisfiability in Alternating-Time Temporal Logic / G. van Drimmelen
Strong Bisimilarity on Basic Parallel Processes Is PSPACE-Complete / P. Jancar
Invited Tutorial--Logic in Access Control / M. AbadiSession 10:
The Planning Spectrum--One, Two, Three, Infinity / M. Pistore ; M. Y. VardiSession 11:
Invited Talk--Advice about Logical AI / J. McCarthy
A Sound Framework for Untrusted Verification-Condition Generators / G. C. Necula ; R. R. SchneckSession 12:
An NP Decision Procedure for Protocol Insecurity with XOR / Y. Chevalier ; R. Kusters ; M. Rusinowitch ; M. Turuani
Intruder Deductions, Constraint Solving and Insecurity Decision in Presence of Exclusive or / H. Comon-Lundh ; V. Shmatikov
Spectrum Hierarchies and Subdiagonal Functions / A. HunterSession 13:
Spectra of Monadic Second-Order Formulas with One Unary Function / Y. Gurevich ; S. Shelah
Convergence Law for Random Graphs with Specified Degree Sequence / J. F. Lynch
Homomorphism Closed vs. Existential Positive / T. FederSession 14:
Tractable Conservative Constraint Satisfaction Problems / A. A. Bulatov
A Constraint-Based Presentation and Generalization of Rows / F. Pottier
Labelled Markov Processes: Stronger and Faster Approximations / V. Danos ; J. DesharnaisSession 15:
Invited Talk--Model Checking for Probability and Time: From Theory to Practice / M. Kwiatkowska
Model Checking Guarded Protocols / E. A. Emerson ; V. KahlonSession 16:
Model-Checking Trace Event Structures / P. Madhusudan
Micro-Macro Stack Systems: A New Frontier of Elementary Decidability for Sequential Systems / N. Piterman
A Proposal to Extend Abstract State Machines to Applications in Systems Biology / Short Presentations II:
Stuttering Refinement on Partial Systems / S. Nejati ; A. Gurfinkel
Assume-Guarantee Reasoning with Features / B. Devereux
Modularity Theorems for Non-Monotone Induction / M. Denecker ; E. Ternovska
Linear-Time Algorithms for Monadic Logic / S. Lindell
Game-Based Notions of Locality / M. Arenas ; P. Barcelo
Arb: An Implementation of Selecting Tree Automata for XML Query Processing
Author Index
Foreword
Conference Organization
Program Committee
5.

図書

図書
sponsored by IEEE Computer Society Technical Committee on the Mathematical Foundations of Computing ; in cooperation with Association for Symbolic Logic and European Association for Theoretical Computer Science
出版情報: Los Alamitos, Calif. ; Tokyo : IEEE Computer Society, c2000  xiii, 425 p. ; 28 cm
所蔵情報: loading…
目次情報: 続きを見る
Conference Organizers
Program Committee
Additional Reviewers
Kleene Award for Best Student Paper
Author Index
Logic, Complexity, and Games / R. Fagin
A General Notion of Realizability / L. Birkedal
A Model for Impredicative Type Systems, Universes, Intersection Types and Subtyping / A. Miquel
Complete Axioms for Categorical Fixed-Point Operators / A. Simpson ; G. Plotkin
The Role of Decidability in First Order Separations over Classes of Finite Structures / S. Lindell ; S. Weinstein
Automatic Structures / A. Blumensath ; E. Gradel
Definability and Compression / F. Afrati ; H. Leiss ; M. de Rougemont
Resource-Bounded Continuity and Sequentiality for Type-Two Functionals / S. Buss ; B. Kapron
A Syntactical Analysis of Non-Size-Increasing Polynomial Time Computation / K. Aehlig ; H. Schwichtenberg
Approximating Labeled Markov Processes / J. Desharnais ; R. Jagadeesan ; V. Gupta ; P. Panangaden
Precongruence Formats for Decorated Trace Preorders / B. Bloom ; W. Fokkink ; R. van Glabbeek
Virtual Symmetry Reduction / E. Emerson ; J. Havlicek ; R. Trefler
Better is Better than Well: On Efficient Verification of Infinite-State Systems / P. Abdulla ; A. Nylen
Concurrent Omega-Regular Games / L. de Alfaro ; T. Henzinger
Approximate Pattern Matching is Expressible in Transitive Closure Logic / K. Lemstrom ; L. Hella
Computational Complexity of Some Problems Involving Congruences on Algebras / C. Bergman ; G. Slutzki
From the Church-Turing Thesis to the First-Order Algorithm Theorem / S. Kripke
Satisfiability Testing: Recent Developments and Challenge Problems / B. Selman
Dominator Trees and Fast Verification of Proof Nets / A. Murawski ; C.-H. Ong
Game Semantics and Subtyping / J. Chroboczek
Probabilistic Game Semantics / V. Danos ; R. Harmer
Back and Forth between Guarded and Modal Logics / C. Hirsch ; M. Otto
More Past Glories / M. Reynolds
A Complete Axiomatization of Interval Temporal Logic with Infinite Time / B. Moszkowski
A Modality for Recurison / H. Nakano
A Static Calculus of Dependencies for the [lambda]-Cube / F. Prost
A Decision Procedure for Term Algebras with Queues / T. Rybina ; A. Voronkov
A Decision Procedure for the Existential Theory of Term Algebras with the Knuth-Bendix Ordering / K. Korovin
Some Strategies for Proving Theorems with a Model Checker / K. McMillan
The Curry-Howard Correspondence in Set Theory / J.-L. Krivine
A Theory of Bisimulation for a Fragment of Concurrent ML with Local Names / A. Jeffrey ; J. Rathke
Models for Name-Passing Processes: Interleaving and Causal / G. Cattani ; P. Sewell
Assigning Types to Processes / N. Yoshida ; M. Hennessy
On First-Order Topological Queries / M. Grohe ; L. Segoufin
View-Based Query Processing and Constraint Satisfaction / D. Calvanese ; G. De Giacomo ; M. Lenzerini ; M. Vardi
Imperative Programming with Dependent Types / H. Xi
Efficient and Flexible Matching of Recursive Types / J. Palsberg ; T. Zhao
How to Optimize Proof-Search in Modal Logics: A New Way of Proving Redundancy Criteria for Sequent Calculi
Paramodulation with Built-in Abelian Groups / G. Godoy ; R. Nieuwenhuis
Conference Organizers
Program Committee
Additional Reviewers
6.

図書

図書
sponsored by IEEE Computer Society Technical Committee on Mathematical Foundations of Computing ; in cooperation with Association of Symbolic Logic, European Association for Theoretical Computer Science ; with support from US Office of Naval Research International Field Office, European Office of Aerospace Research and Development of the US Air Force Office of Scientific Research
出版情報: Los Alamitos, Calif. : IEEE Computer Society, c2002  xiii, 461 p. ; 28 cm
所蔵情報: loading…
目次情報: 続きを見る
Foreword
Conference Organisers
Programme Committee
Additional Reviewers
FLoC Joint Invited Lecture
Little Engines of Proof / N. Shankar
Automatic Decidability / C. Lynch ; B. MorawskaSession 1:
Tree-Like Counterexamples in Model Checking / E. Clarke ; S. Jha ; Y. Lu ; H. VeithSession 2:
Probabilistic Abstraction for Model Checking: An Approach Based on Property Testing / S. Laplante ; R. Lassaigne ; F. Magniez ; S. Peyronnet ; M. de Rougemont
Semantic Minimization of 3-Valued Propositional Formulae / T. Reps ; A. Loginov ; M. Sagiv
Invited Lecture: Separation Logic: A Logic for Shared Mutable Data Structures / J. C. ReynoldsSession 3:
A Stratified Semantics of General References Embeddable in Higher-Order Logic / A. J. Ahmed ; A. W. Appel ; R. Virga
A Syntactic Approach to Foundational Proof-Carrying Code / N. A. Hamid ; Z. Shao ; V. Trifonov ; S. Monnier ; Z. NiSession 4:
A Fully Abstract May Testing Semantics for Concurrent Objects / A. Jeffrey ; J. Rathke
Semantics and Logic of Object Calculi / B. Reus ; T. Streicher
Efficient Type Inference for Record Concatenation and Subtyping / J. Palsberg ; T. ZhaoSession 5:
Semantic Subtyping / A. Frisch ; G. Castagna ; V. Benzaken
Remarks on Isomorphisms in Typed Lambda Calculi with Empty and Sum Types / M. Fiore ; R. Di Cosmo ; V. Balat
On the Lambda Y Calculus / R. StatmanSession 6:
Dense Real-Time Games / M. Faella ; S. La Torre ; A. Murano
Computing Reachability Relations in Timed Automata / C. Dima
Invited Lecture: Monadic Queries over Tree-Structured Data / G. Gottlob ; C. KochSession 7:
Tree Extension Algebras: Logics, Automata, and Query Languages / M. Benedikt ; L. Libkin
The Complexity of First-Order and Monadic Second-Order Logic Revisited / M. Frick ; M. GroheSession 8:
The 0-1 Law Fails for Frame Satisfiability of Propositional Modal Logic / J.-M. Le Bars
Some Results on Automatic Structures / H. Ishihara ; B. Khoussainov ; S. Rubin
Observational Equivalence of 3rd-Order Idealized Algol is Decidable / C.-H. L. OngSession 9:
Games on Graphs and Sequentially Realizable Functionals / M. Hyland ; A. Schalk
Polarized Games / O. Laurent
Domain Theory and Differential Calculus (Functions of One Variable) / A. Edalat ; A. LieutierSession 10:
Computational Adequacy for Recursive Types in Models of Intuitionistic Set Theory / A. Simpson
The Powerdomain of Indexed Valuations / D. Varacca
Invited Lecture: Complexity Classes, Propositional Proof Systems, and Formal Theories / S. A. CookSession 11:
Complete Problems for Dynamic Complexity Classes / W. Hesse ; N. Immerman
Unsatisfiable Random Formulas Are Hard to Certify / A. AtseriasSession 12:
The Proof Complexity of Linear Algebra / M. Soltys ; S. Cook
Calibrating Computational Feasibility by Abstraction Rank / D. Leivant
Short Presentations / Session 13:
Lessons Learned from Formal Developments in PVS / J. Ford ; I. A. Mason
CLP Implementation of a Phase Model Checker / S. Soliman
An Overview of MR, a Calculus of Mobile Resources / J. C. Godskesen ; T. Hildebrandt ; V. Sassone
Ludics Dynamics: Designs and Interactive Observability / C. Faggian
Invited Tutorial: Description Logics: Foundations for Class-Based Knowledge Representation / D. Calvanese ; G. De Giacomo ; M. LenzeriniSession 14:
Modal and Guarded Characterisation Theorems over Finite Transition Systems / M. Otto
Temporal Logic with Forgettable Past / F. Laroussinie ; N. Markey ; P. SchnoebelenSession 15:
Decidable and Undecidable Fragments of First-Order Branching Temporal Logics / I. Hodkinson ; F. Wolter ; M. Zakharyaschev
Expressive Equivalence of Least and Inflationary Fixed-Point Logic / S. Kreutzer
The Metric Analogue of Weak Bisimulation for Probabilistic Processes / J. Desharnais ; R. Jagadeesan ; V. Gupta ; P. PanangadenSession 16:
Separability, Expressiveness, and Decidability in the Ambient Logic / D. Hirschkoff ; E. Lozes ; D. Sangiorgi
Linearity in Process Languages / M. Nygaard ; G. Winskel
Deciding Confluence of Certain Term Rewriting Systems in Polynomial Time / A. TiwariSession 17:
Two Adversary Lower Bounds for Parity Games / H. Bjorklund ; S. Vorobyov
Is Randomized Gurvich-Karzanov-Khachiyan's Algorithm for Parity Games Polynomial? / E. Beffara
Time-Space Computational Complexity of Imperative Programming Languages / E. Covino ; G. Pani
Author Index
Foreword
Conference Organisers
Programme Committee
文献の複写および貸借の依頼を行う
 文献複写・貸借依頼