Foundations of Software Science and Computation Structure
2005
- Branching Cells as Local States for Event Structures and Nets: Probabilistic Applicationsby: Samy Abbes, Albert Benveniste
- Mathematical Models of Computational and Combinatorial Structuresby: Marcelo P. Fiore
- Expressivity of Coalgebraic Modal Logic: The Limits and Beyondby: Lutz Schröder
- Bisimulation on Speed: A Unified Approachby: Gerald Lüttgen, Walter Vogler
- A Category of Higher-Dimensional Automataby: Ulrich Fahrenberg
- Duality for Logics of Transition Systemsby: Marcello M. Bonsangue, Alexander Kurz
- Axiomatizations for Probabilistic Finite-State Behaviorsby: Yuxin Deng, Catuscia Palamidessi
- From Separation Logic to First-Order Logicby: Cristiano Calcagno, Philippa Gardner, Matthew Hague
- A Simpler Proof Theory for Nominal Logicby: James Cheney
- The Complexity of Live Sequence Chartsby: Yves Bontemps, Pierre-Yves Schobbens
- Justifying Algorithms for beta-eta-Conversionby: Healfdene Goguen
- Fault Diagnosis Using Timed Automataby: Patricia Bouyer, Fabrice Chevalier, Deepak D'Souza
- On Decidability Within the Arithmetic of Addition and Divisibilityby: Marius Bozga, Radu Iosif
- Composition and Decomposition in True-Concurrencyby: Sibylle B. Fröschle
- Foundations of Web Transactionsby: Cosimo Laneve, Gianluigi Zavattaro
- Stochastic Transition Systems for Continuous State Spaces and Non-determinismby: Stefano Cattani, Roberto Segala, Marta Z. Kwiatkowska, Gethin Norman
- Model Checking for Nominal Calculiby: Gian Luigi Ferrari, Ugo Montanari, Emilio Tuosto
- Component Refinement and CSC Solving for STG Decompositionby: Mark Schäfer, Walter Vogler
- Congruence for Structural Congruencesby: Mohammad Reza Mousavi, Michel A. Reniers
- A Computational Model for Multi-variable Differential Calculusby: Abbas Edalat, André Lieutier, Dirk Pattinson
- Model Checking Durational Probabilistic Systemsby: François Laroussinie, Jeremy Sproston
- History-Based Access Control with Local Policiesby: Massimo Bartoletti, Pierpaolo Degano, Gian Luigi Ferrari
- Free-Algebra Models for the pi-Calculusby: Ian Stark
- A Unifying Model of Variables and Namesby: Marino Miculan, Kidane Yemane
- Probabilistic Congruence for Semistochastic Generative Processesby: Ruggero Lanotte, Simone Tini
- Optimal Conditional Reachability for Multi-priced Timed Automataby: Kim Guldstrand Larsen, Jacob Illum Rasmussen
- Bridging Language-Based and Process Calculi Securityby: Riccardo Focardi, Sabina Rossi, Andrei Sabelfeld
- Confluence of Right Ground Term Rewriting Systems Is Decidableby: Lukasz Kaiser
- Safety Is not a Restriction at Level 2 for String Languagesby: Klaus Aehlig, Jolie G. de Miranda, C.-H. Luke Ong
- Full Abstraction for Polymorphic Pi-Calculusby: Alan Jeffrey, Julian Rathke
- Third-Order Idealized Algol with Iteration Is Decidableby: Andrzej S. Murawski, Igor Walukiewicz
- Alternating Timed Automataby: Slawomir Lasota, Igor Walukiewicz
- Choice in Dynamic Linkingby: Martín Abadi, Georges Gonthier, Benjamin Werner
- Partial Correctness Assertions Provable in Dynamic Logicsby: Daniel Leivant
- Intruder Theories (Ongoing Work)by: Hubert Comon-Lundh
- Electoral Systems in Ambient Calculiby: Iain Phillips, Maria Grazia Vigliotti
- Tree Transducers and Tree Compressionsby: Sebastian Maneth, Giorgio Busatto
- On Term Rewriting Systems Having a Rational Derivationby: Antoine Meyer
- On Finite Alphabets and Infinite Bases: From Ready Pairs to Possible Worldsby: Wan Fokkink, Sumit Nain
- Soft lambda-Calculus: A Language for Polynomial Time Computationby: Patrick Baillot, Virgile Mogbil
- Strong Normalization of lambda-mu-mu/tilde-Calculus with Explicit Substitutionsby: Emmanuel Polonovski
- Angelic Semantics of Fine-Grained Concurrencyby: Dan R. Ghica, Andrzej S. Murawski
- Theories for the Global Ubiquitous Computerby: Robin Milner
- Adhesive Categoriesby: Stephen Lack, Pawel Sobocinski
- Election and Local Computations on Edgesby: Jérémie Chalopin, Yves Métivier
- Deriving Bisimulation Congruences in the DPO Approach to Graph Rewritingby: Hartmut Ehrig, Barbara König
- On Recognizable Timed Languagesby: Oded Maler, Amir Pnueli
- Perfect-Information Stochastic Parity Gamesby: Wieslaw Zielonka
- A Note on the Perfect Encryption Assumption in a Process Calculusby: Roberto Zunino, Pierpaolo Degano
- Unifying Recursive and Co-recursive Definitions in Sheaf Categoriesby: Pietro Di Gianantonio, Marino Miculan
- Duality for Labelled Markov Processesby: Michael W. Mislove, Joël Ouaknine, Dusko Pavlovic, James Worrell
- Bisimulation on Speed: Lower Time Boundsby: Gerald Lüttgen, Walter Vogler
- Polynomials for Proving Termination of Context-Sensitive Rewritingby: Salvador Lucas
- On the Expressiveness of Infinite Behavior and Name Scoping in Process Calculiby: Pablo Giambiagi, Gerardo Schneider, Frank D. Valencia
- A Denotational Account of Untyped Normalization by Evaluationby: Andrzej Filinski, Henning Korsholm Rohde
- Strong Bisimulation for the Explicit Fusion Calculusby: Lucian Wischik, Philippa Gardner
- Specifying and Verifying Partial Order Properties Using Template MSCsby: Blaise Genest, Marius Minea, Anca Muscholl, Doron Peled
- Behavioral and Spatial Observations in a Logic for the pi-Calculusby: Luís Caires
- Hypergraphs and Degrees of Parallelism: A Completeness Resultby: Antonio Bucciarelli, Benjamin Leperchey
- Canonical Models for Computational Effectsby: John Power
- Decidability of Freshness, Undecidability of Revelationby: Giovanni Conforti, Giorgio Ghelli
- On the Existence of an Effective and Complete Inference System for Cryptographic Protocolsby: Liana Bozga, Cristian Ene, Yassine Lakhnech
- Distance Desert Automata and the Star Height One Problemby: Daniel Kirsten
- Probabilistic Bisimulation and Equivalence for Security Analysis of Network Protocolsby: Ajith Ramanathan, John C. Mitchell, Andre Scedrov, Vanessa Teague
- LTL over Integer Periodicity Constraints: (Extended Abstract)by: Stéphane Demri
- safeDpi: A Language for Controlling Mobile Codeby: Matthew Hennessy, Julian Rathke, Nobuko Yoshida
- A Game Semantics of Local Names and Good Variablesby: James Laird
- Reasoning about Dynamic Policiesby: Riccardo Pucella, Vicky Weissman
- A Monadic Multi-stage Metalanguageby: Eugenio Moggi, Sonia Fagorzi
- Multi-level Meta-reasoning with Higher-Order Abstract Syntaxby: Alberto Momigliano, Simon Ambler
- Computability over an Arbitrary Structure. Sequential and Parallel Polynomial Timeby: Olivier Bournez, Felipe Cucker, Paulin Jacobé de Naurois, Jean-Yves Marion
- Abstraction in Reasoning about Higraph-Based Systemsby: John Power, Konstantinos Tourlas
- Model Checking Lossy Channels Systems Is Probably Decidableby: Nathalie Bertrand, Ph. Schnoebelen
- A Normalisation Result for Higher-Order Calculi with Explicit Substitutionsby: Eduardo Bonelli
- When Ambients Cannot Be Openedby: Iovka Boneva, Jean-Marc Talbot
- Counting and Equality Constraints for Multitree Automataby: Denis Lugiez
- The Converse of a Stochastic Relationby: Ernst-Erich Doberkat
- Verification of Cryptographic Protocols: Tagging Enforces Terminationby: Bruno Blanchet, Andreas Podelski
- An Intrinsic Characterization of Approximate Probabilistic Bisimilarityby: Franck van Breugel, Michael W. Mislove, Joël Ouaknine, James Worrell
- Deriving Bisimulation Congruences: 2-Categories Vs Precategoriesby: Vladimiro Sassone, Pawel Sobocinski
- A Game Semantics of Linearly Used Continuationsby: James Laird
- Manipulating Trees with Hidden Labelsby: Luca Cardelli, Philippa Gardner, Giorgio Ghelli
- Type Assignment for Intersections and Unions in Call-by-Value Languagesby: Joshua Dunfield, Frank Pfenning
- Compositional Circular Assume-Guarantee Rules Cannot Be Sound and Completeby: Patrick Maier
- Verification of Probabilistic Systems with Faulty Communicationby: Parosh Aziz Abdulla, Alexander Moshe Rabinovich
- Categories of Containersby: Michael Abbott, Thorsten Altenkirch, Neil Ghani
- Ambiguous Classes in the Games µ-Calculus Hierarchyby: André Arnold, Luigi Santocanale
- A Game Semantics for Generic Polymorphismby: Samson Abramsky, Radha Jagadeesan
- On the Structure of Inductive Reasoning: Circular and Tree-Shaped Proofs in the µ-Calculusby: Christoph Sprenger, Mads Dam
- Parameterized Verification by Probabilistic Abstractionby: Tamarah Arons, Amir Pnueli, Lenore D. Zuck
- The Two-Variable Guarded Fragment with Transitive Guards Is 2EXPTIME-Hardby: Emanuel Kieronski
- Towards a Behavioural Theory of Access and Mobility Control in Distributed Systemsby: Matthew Hennessy, Massimo Merro, Julian Rathke
- Genericity and the pi-Calculusby: Martin Berger, Kohei Honda, Nobuko Yoshida
- Generalized Iteration and Coiteration for Higher-Order Nested Datatypesby: Andreas Abel, Ralph Matthes, Tarmo Uustalu
- Cones and Foci for Protocol Verification Revisitedby: Wan Fokkink, Jun Pang
- On Specification Logics for Algebra-Coalgebra Structures: Reconciling Reachability and Observabilityby: Corina Cîrstea
- Heterogeneous Development Graphs and Heterogeneous Borrowingby: Till Mossakowski
- Verifying Temporal Properties Using Explicit Approximants: Completeness for Context-free Processesby: Ulrich Schöpp, Alex K. Simpson
- Logics Admitting Final Semanticsby: Alexander Kurz
- On Model Checking Durational Kripke Structuresby: François Laroussinie, Nicolas Markey, Ph. Schnoebelen
- Equivalence-Checking with One-Counter Automata: A Generic Method for Proving Lower Boundsby: Petr Jancar, Antonín Kucera, Faron Moller, Zdenek Sawa
- The Informatic Derivative at a Compact Elementby: Keye Martin
- Bounded MSC Communicationby: Markus Lohrey, Anca Muscholl
- Note on the Tableau Technique for Commutative Transition Systemsby: Jirí Srba
- Efficient Type Matchingby: Somesh Jha, Jens Palsberg, Tian Zhao
- On Compositional Reasoning in the Spi-calculusby: Michele Boreale, Daniele Gorla
- Verification for Java's Reentrant Multithreading Conceptby: Erika Ábrahám-Mumm, Frank S. de Boer, Willem P. de Roever, Martin Steffen
- On the Integration of Observability and Reachability Conceptsby: Michel Bidoit, Rolf Hennicker
- The Demonic Product of Probabilistic Relationsby: Ernst-Erich Doberkat
- A Semantic Basis for Local Reasoningby: Hongseok Yang, Peter W. O'Hearn
- Model-Checking Infinite Systems Generated by Ground Tree Rewritingby: Christof Löding
- Higher-Order Pushdown Trees Are Easyby: Teodor Knapik, Damian Niwinski, Pawel Urzyczyn
- Proving Correctness of Timed Concurrent Constraint Programsby: Frank S. de Boer, Maurizio Gabbrielli, Maria Chiara Meo
- Linearity and Bisimulationby: Nobuko Yoshida, Kohei Honda, Martin Berger
- Model Checking Fixed Point Logic with Chopby: Martin Lange, Colin Stirling
- Notions of Computation Determine Monadsby: Gordon D. Plotkin, John Power
- A Calculus of Circular Proofs and Its Categorical Semanticsby: Luigi Santocanale
- A Characterization of Families of Graphs in Which Election Is Possibleby: Emmanuel Godard, Yves Métivier
- Minimizing Transition Systems for Name Passing Calculi: A Co-algebraic Formulationby: Gian Luigi Ferrari, Ugo Montanari, Marco Pistore
- Generalised Regular MSC Languagesby: Benedikt Bollig, Martin Leucker, Thomas Noll
- A First-Order One-Pass CPS Transformationby: Olivier Danvy, Lasse R. Nielsen
- Varieties of Effectsby: Carsten Führmann
- Semantical Evaluations as Monadic Second-Order Compatible Structure Transformationsby: Bruno Courcelle
- Conflict Detection and Resolution in Access Control Policy Specificationsby: Manuel Koch, Luigi V. Mancini, Francesco Parisi-Presicce
- Class Analysis of Object-Oriented Programs through Abstract Interpretationby: Thomas P. Jensen, Fausto Spoto
- The Finite Graph Problem for Two-Way Alternating Automataby: Mikolaj Bojanczyk
- On the Complexity of Parity Word Automataby: Valerie King, Orna Kupferman, Moshe Y. Vardi
- Decidability of Weak Bisimilarity for a Subset of Basic Parallel Processesby: Colin Stirling
- Model Checking CTL+ and FCTL is Hardby: François Laroussinie, Nicolas Markey, Ph. Schnoebelen
- High-Level Petri Nets as Type Theories in the Join Calculusby: Maria Grazia Buscemi, Vladimiro Sassone
- Categories of Processes Enriched in Final Coalgebrasby: Sava Krstic, John Launchbury, Dusko Pavlovic
- An Axiomatic Semantics for the Synchronous Language Gentzenby: Simone Tini
- Synchronized Tree Languages Revisited and New Applicationsby: Valérie Gouranton, Pierre Réty, Helmut Seidl
- MARRELLA and the Verification of an Embedded Systemby: Dominique Ambroise, Patrick Augé, Kamel Bouchefra, Brigitte Rozoy
- Type Inference with Recursive Type Equationsby: Mario Coppo
- Axiomatizing Tropical Semiringsby: Luca Aceto, Zoltán Ésik, Anna Ingólfsdóttir
- Temporary Data in Shared Dataspace Coordination Languagesby: Nadia Busi, Roberto Gorrieri, Gianluigi Zavattaro
- Axioms for Recursion in Call-by-Valueby: Masahito Hasegawa, Yoshihiko Kakutani
- Adequacy for Algebraic Effectsby: Gordon D. Plotkin, John Power
- On the Modularity of Deciding Call-by-Needby: Irène Durand, Aart Middeldorp
- The Rho Cubeby: Horatiu Cirstea, Claude Kirchner, Luigi Liquori
- Type Isomorphisms and Proof Reuse in Dependent Type Theoryby: Gilles Barthe, Olivier Pons
- On Garbage and Program Logicby: Cristiano Calcagno, Peter W. O'Hearn
- Foundations for a Graph-Based Approach to the Specification of Access Control Policiesby: Manuel Koch, Luigi V. Mancini, Francesco Parisi-Presicce
- On Regular Message Sequence Chart Languages and Relationships to Mazurkiewicz Trace Theoryby: Rémi Morin
- The Complexity of Model Checking Mobile Ambientsby: Witold Charatonik, Silvano Dal-Zilio, Andrew D. Gordon, Supratik Mukhopadhyay, Jean-Marc Talbot
- Verified Bytecode Verifiersby: Tobias Nipkow
- Secrecy Types for Asymmetric Communicationby: Martín Abadi, Bruno Blanchet
- Higher-Order Abstract Syntax with Induction in Isabelle/HOL: Formalizing the pi-Calculus and Mechanizing the Theory of Contextsby: Christine Röckl, Daniel Hirschkoff, Stefan Berghofer
- Computational Completeness of Programming Languages Based on Graph Transformationby: Annegret Habel, Detlef Plump
- On the Duality between Observability and Reachabilityby: Michel Bidoit, Rolf Hennicker, Alexander Kurz
- Constructive Data Refinement in Typed Lambda Calculusby: Furio Honsell, John Longley, Donald Sannella, Andrzej Tarlecki
- Type Inference for First-Order Logicby: Aleksy Schubert
- The State Explosion Problem from Trace to Bisimulation Equivalenceby: François Laroussinie, Ph. Schnoebelen
- Subtyping and Typing Algorithms for Mobile Ambientsby: Pascal Zimmer
- A Higher-Order Simulation Relation for System Fby: Jo Erskine Hannay
- A Proof System for Timed Automataby: Huimin Lin, Wang Yi
- Sequential and Concurrent Abstract Machines for Interaction Netsby: Jorge Sousa Pinto
- On Rational Graphsby: Christophe Morvan
- On Word Rewriting Systems Having a Rational Derivationby: Didier Caucal
- Predicate Logic and Tree Automata with Testsby: Ralf Treinen
- Verifying Performance Equivalence for Timed Basic Parallel Processesby: Béatrice Bérard, Anne Labroue, Ph. Schnoebelen
- Compositional Verification in Linear-Time Temporal Logicby: Yih-Kuen Tsay
- On Recognizable Stable Trace Languagesby: Jean-François Husson, Rémi Morin
- Probabilistic Asynchronous pi-Calculusby: Oltea Mihaela Herescu, Catuscia Palamidessi
- On the Semantics of Refinement Calculiby: Hongseok Yang, Uday S. Reddy
- Hierarchical Graph Transformationby: Frank Drewes, Berthold Hoffmann, Detlef Plump
- Norm Functions for Probabilistic Bisimulations with Delaysby: Christel Baier, Mariëlle Stoelinga
- An Algebraic Foundation for Adaptive Programmingby: Peter Thiemann
- Categorical Models for Intuitionistic and Linear Type Theoryby: Maria Emilia Maietti, Valeria de Paiva, Eike Ritter
- Proof Nets and Explicit Substitutionsby: Roberto Di Cosmo, Delia Kesner, Emmanuel Polonovski
- Constructor Subtyping in the Calculus of Inductive Constructionsby: Gilles Barthe, Femke van Raamsdonk
- Locality and Polyadicity in Asynchronous Name-Passing Calculiby: Massimo Merro
- A Program Refinement Framework Supporting Reasoning about Knowledge and Timeby: Kai Engelhardt, Ron van der Meyden, Yoram Moses
- On Synchronous and Asynchronous Mobile Processesby: Paola Quaglia, David Walker
- Typing Local Definitions and Conditional Expressions with Rank 2 Intersectionby: Ferruccio Damiani
- Unfolding and Event Structure Semantics for Graph Grammarsby: Paolo Baldan, Andrea Corradini, Ugo Montanari
- A WP-calculus for OOby: Frank S. de Boer
- A pi-calculus Process Semantics of Concurrent Idealised ALGOLby: Christine Röckl, Davide Sangiorgi
- Probabilistic Temporal Logics via the Modal Mu-Calculusby: Murali Narasimha, Rance Cleaveland, S. Purushothaman Iyer
- A Complete Coinductive Logical System for Bisimulation Equivalence on Circular Objectsby: Marina Lenisa
- An Algebraic Characterization of Typability in ML with Subtypingby: Marcin Benke
- String Languages Generated by Total Deterministic Macro Tree Transducersby: Sebastian Maneth
- Testing Hennessy-Milner Logic with Recursionby: Luca Aceto, Anna Ingólfsdóttir
- Categorical Models of Explicit Substitutionsby: Neil Ghani, Valeria de Paiva, Eike Ritter
- The Recognizability Problem for Tree Automata with Comparisons between Brothersby: Bruno Bogaert, Franck Seynhaeve, Sophie Tison
- Reasoning About Concurrent Systems Using Typesby: Davide Sangiorgi
- A Theory of "May" Testing for Asynchronous Languagesby: Michele Boreale, Rocco De Nicola, Rosario Pugliese
- Expanding the Cubeby: Gilles Barthe
- Equational Properties of Mobile Ambientsby: Andrew D. Gordon, Luca Cardelli
- A Nondeterministic Polynomial-Time Unification Algorithm for Bags, Sets and Treesby: Evgeny Dantsin, Andrei Voronkov
- A Strong Logic Programming View for Static Embedded Implicationsby: R. Arruabarrena, P. Lucio, Marisa Navarro
- An Automata-Theoretic Approach to Interprocedural Data-Flow Analysisby: Javier Esparza, Jens Knoop
- Static Analysis of Processes for No and Read-Up nad No Write-Downby: Chiara Bodei, Pierpaolo Degano, Flemming Nielson, Hanne Riis Nielson
- Security Protocols and Specificationsby: Martín Abadi
- Matching Specifications for Message Sequence Chartsby: Anca Muscholl
- Model Checking Logics for Communicating Sequential Agentsby: Michaela Huhn, Peter Niebert, Frank Wallner
- The Appearance of Big Integers in Exact Real Arithmetic Based on Linear Fractional Transformationsby: Reinhold Heckmann
- Pumping Lemmas for Timed Automataby: Danièle Beauquier
- On Piecewise Testable, Starfree, and Recognizable Picture Languagesby: Oliver Matz
- The Church-Rosser Languages Are the Deterministic Variants of the Growing Context-Sensitive Languagesby: Gundula Niemann, Friedrich Otto
- Partial Metrics and Co-continuous Valuationsby: Michael A. Bukatin, Svetlana Yu. Shorina
- Asynchronous Observations of Processesby: Michele Boreale, Rocco De Nicola, Rosario Pugliese
- Deciding Properties for Message Sequence Chartsby: Anca Muscholl, Doron Peled, Zhendong Su
- Resource Based Models for Asynchronyby: Julian Rathke
- Rational Term Rewritingby: Andrea Corradini, Fabio Gadducci
- Deterministic Rational Transducers and Random Sequencesby: Sylvain Porrot, Max Dauchet, Bruno Durand, Nikolai K. Vereshchagin
- A Cook's Tour of Equational Axiomatizations for Prefix Iterationby: Luca Aceto, Wan Fokkink, Anna Ingólfsdóttir
- Mobile Ambientsby: Luca Cardelli, Andrew D. Gordon
- An Event Structure Semantics for P/T Contextual Nets: Asymmetric Event Structuresby: Paolo Baldan, Andrea Corradini, Ugo Montanari
- Analysis of a Guard Condition in Type Theory (Extended Abstract)by: Roberto M. Amadio, Solange Coupet-Grimal
- Generalizing Domain Theoryby: Michael W. Mislove
- The WHILE Hierarchy of Program Schemes Is Infiniteby: Can Adam Albayrak, Thomas Noll
- Functor Categories and Two-Level Languagesby: Eugenio Moggi
- Minor Searching, Normal Forms of Graph Relabelling: Two Applications Based on Enumerations by Graph Relabellingby: Anne Bottreau, Yves Métivier
- Net Refinement by Pullback Rewritingby: Renate Klempien-Hinrichs
![[SWISH++]](/docis/swish-powered.gif){kind=small}
