Département d'Informatique
Laboratoire des Méthodes de Programmation
(LAMP)
Ecole Politechnique Federale de Lausanne

 

Christine Röckl's Bibliography

 Publications

 Journal Papers
 Papers at Conferences and Refereed Workshops
 Workshop Papers

 Theses

 Reports

 Back to my Homepage.

 

 

 Publications

 Journal Papers
[RH03] A Fully Adequate Shallow Embedding of the Pi-Calculus in Isabelle/HOL with Mechanized Syntax Analysis
C. Röckl and D. Hirschkoff. In Journal of Functional Programming, 2003.

Abstract: This paper discusses an application of the higher-order abstract syntax technique to general-purpose theorem proving, yielding shallow embeddings of the binders of formalized languages. Higher-order abstract syntax has been applied with success in specialized logical frameworks which satisfy a closed-world assumption. As more general environments (like Isabelle/HOL or Coq) do not support this closed-world assumption, higher-order abstract syntax may yield exotic terms, that is, datatypes may produce more terms than there should actually be in the language. The work at hand demonstrates how such exotic terms can be eliminated by means of a two-level well-formedness predicate, further preparing the ground for an implementation of structural induction in terms of rule induction, and hence providing fully-fledged syntax analysis. In order to apply and justify well-formedness predicates, the paper develops a proof technique based on a combination of instantiations and reabstractions of higher-order terms. As an application, syntactic principles like the theory of contexts (as introduced by Honsell, Miculan, and Scagnetto) are derived, and adequacy of the predicates is shown, both within a formalization of the pi-calculus in Isabelle/HOL.

@Article{Roeckl::Hirschkoff::2003,
  author = 	 {C. R\"ockl and D. Hirschkoff},
  title =        {A Fully Adequate Shallow Embedding of the $\pi$-Calculus
                in {Isabelle/HOL} with Mechanized Syntax Analysis},
  journal =      {Journal of Functional Programming},
  year =         2003
}
 Papers at Conferences and Refereed Workshops
[RS99] A Pi-Calculus Process Semantics of Concurrent Idealized ALGOL.
C. Röckl and D. Sangiorgi. In Proc. FOSSACS'99, LNCS 1578, pages 306-321. Springer, 1999.

Abstract: We study the use of the pi-calculus for semantical descriptions of languages such as Concurrent Idealised ALGOL (CIA), combining imperative, functional and concurrent features. We first present an operational semantics for CIA, given by SOS rules and a contextual form of behavioural equivalence; then a pi-calculus semantics. As behavioural equivalence on pi-calculus processes we choose the standard (weak early) bisimilarity. We comparethe two semantics, demonstrating that there is a close operational correspondence between them and that the pi-calculus semantics is sound. This allows for applying the pi-calculus theory in proving behavioural properties of CIA phrases. We discuss laws and examples which have served as benchmarks to various semantics, and a more complex example involving procedures of higher order.

@InProceedings{Roeckl::Sangiorgi::1999,
  author = 	 {C. R\"ockl and D. Sangiorgi},
  title = 	 {A $\pi$-calculus Process Semantics of
                  Concurrent Idealised {ALGOL}},
  booktitle = 	 {Proc. FOSSACS'99},
  pages =	 {306--321},
  year =	 1999,
  editor =	 {W. Thomas},
  volume =	 1578,
  series =	 {Lecture Notes in Computer Science},
  publisher =	 {Springer}
}

[ps]
[RE99] Proof-Checking Protocols Using Bisimulations.
C. Röckl and J. Esparza. In Proc. CONCUR'99, LNCS 1664, pages 525-540. Springer, 1999.

Abstract: Observation equivalence is of particular interest to the verification of concurrent systems, as it is compositional, detects deadlocks, and possesses a well-developed theory. We examine the mechanization of proofs by exhibiting bisimulation relations. As examples we have chosen infinite-state, as well as parameterized systems, that cannot be treated by fully automatic tools based on exploring the complete state space. The description of the systems is given by a transition semantics based on value-passing processes, though automata models, for instance, would be equally applicable. For the mechanization, we use the interactive theorem prover Isabelle/HOL, as it enables the user to apply inductive definitions and proofs, and provides powerful built-in proof tactics.

@InProceedings{Roeckl::Esparza::1999,
  author = 	 {C. R\"ockl and J. Esparza},
  title = 	 {Proof-Checking Protocols using Bisimulations},
  booktitle = 	 {Proc. CONCUR'99},
  pages =	 {525--540},
  year =	 1999,
  editor =	 {J.C.M. Baeten and S. Mauw},
  volume =	 1664,
  series =	 {Lecture Notes in Computer Science},
  publisher =	 {Springer}
}

[ps] [proof-scripts]
[RHB01] Higher-Order Abstract Syntax with Induction in Isabelle/HOL: Formalizing the Pi-Calculus and Mechanizing the Theory of Contexts.
C. Röckl and D. Hirschkoff and S. Berghofer. In Proc. FOSSACS'01, LNCS 2030. Springer, 2001.

Abstract: Higher-order abstract syntax is a natural way to formalize programming languages with binders, like the pi-calculus, because alpha-conversion, instantiations and capture avoidance are delegated to the meta-level of the provers, making tedious substitutions superfluous. However, such formalizations usually lack structural induction, which makes syntax-analysis impossible. Moreover, when applied in logical frameworks with object-logics, like Isabelle/HOL or standard extensions of Coq, exotic terms can be defined, for which important syntactic properties become invalid.
The paper presents a formalization of the pi-calculus in Isabelle/HOL, using well-formedness predicates which both eliminate exotic terms and yield structural induction. These induction-principles are then used to derive the Theory of Contexts fully within the mechanization.

@InProceedings{Roeckl::Hirschkoff::Berghofer::2001,
  author = 	 {C. R\"ockl and D. Hirschkoff and S. Berghofer},
  title = 	 {Higher-Order Abstract Syntax with Induction
                  in {Isabelle/HOL}: Formalizing the Pi-Calculus and
                  Mechanizing the Theory of Contexts},
  booktitle = 	 {Proc. FOSSACS'01},
  pages =	 {364--378},
  year =	 2001,
  editor =	 {F. Honsell and M. Miculan},
  volume =	 {2030},
  series =	 {Lecture Notes in Computer Science},
  publisher =	 {Springer}
}

[ps] [proof-scripts]
[Roe01b] A First-Order Syntax for the Pi-Calculus in Isabelle/HOL using Permutations.
C. Röckl. In Proc. MERLIN'01, ENTCS 58.1. Elsevier, 2001.

Abstract: A formalized theory of alpha-conversion for the pi-calculus in Isabelle/HOL is presented. Following a recent proposal by Gabbay and Pitts, substitutions are modelled in terms of permutations, and alpha-equivalence is defined over all but finitely many names. In contrast to the work by Gabbay and Pitts, however, standard universal and existential quantification are used instead of introducing a new binder. Further, a classification of the various approaches to formalizing languages with binders is presented. Strengths and weaknesses are pointed out, and suggestions for possible applications are made.

@InProceedings{Roeckl::2001b,
  author = 	 {C. R\"ockl},
  title = 	 {A First-Order Syntax for the Pi-Calculus in
                  {Isabelle/HOL} using Permutations},
  booktitle = 	 {Proc. MERLIN'01},
  year =	 2001,
  editor =	 {S. Ambler and R. Crole and A. Momigliano},
  volume =	 {58.1},
  series =	 {ENTCS},
  publisher =	 {Elsevier}
}

[ps] [proof-scripts]
[OCRZ03] A Nominal Theory of Objects with Dependent Types
M. Odersky, V. Cremet, C. Röckl, M. Zenger. In Proc. FOOL'03, 2003.

Abstract: We design and study newObj, a calculus and dependent type system for objects and classes which can have types as members. Type members can be aliases, abstract types, or new types. The type system can model the essential concepts of JavaBETA or gbeta. It can also model most concepts of SML-style module systems, including sharing constraints and higher-order functors, but excluding applicative functors. The type system can thus be used as a basis for unifying concepts that so far existed in parallel in advanced object systems and in module systems. The technical report presents results on confluence of the calculus, soundness of the type system, and undecidability of type checking.

@InProceedings{Odersky::Cremet::Roeckl::Zenger::2002,
  author = 	 {M. Odersky and V. Cremet and C. R\"ockl and M. Zenger},
  title = 	 {A Nominal Theory of Objects with Dependent Types},
  booktitle =    {Proc. FOOL'03},
  year = 	 2003
}

[pdf]

 Workshop Papers
[Roe99] First-Order Proofs for Higher-Order Languages.
C. Röckl. In Proc. FBT'99, pages 193-202. Utz, 1999.

Abstract: We study the use of the pi-calculus for semantical descriptions of higher-order concurrent languages with state. As an example, we choose Concurrent Idealized ALGOL (CIA). CIA is particularly interesting as, yet being a core language, it combines imperative and parallel features with a procedural mechanism of full higher order. It can thus be used as a formal model for concurrent programs as, e.g., remote procedure calls or remote execution of program parts. However, deriving congruence laws for languages of this kind is hard, as they combine higher order with local state. In order to conduct proofs of laws and examples in a first-order environment, we encode CIA in the pi-calculus, exploiting results that its mobility allows a first-order description of higher order. Moreover, by translating CIA into , we can make use of the various proof techniques that have been developed for the calculus.

@InProceedings{Roeckl::1999,
  author = 	 {C. R\"ockl},
  title = 	 {First-Order Proofs for Higher-Order Languages},
  booktitle = 	 {Proc. FBT'99},
  pages =	 {193--202},
  year =	 1999,
  editor =	 {B. Sch\"atz and K. Spies},
  publisher =	 {Utz}
}

[ps]
[Roe00] Proving Write-Invalidate Cache-Coherence with Bisimulations in Isabelle/HOL.
C. Röckl. In Proc. FBT'00, pages 69-78. Shaker, 1999.

Abstract: The aim of this paper is to advocate the use of bisimulation relations in the verification of infinite-state or parameterized systems, and demonstrates the support that general-purpose theorem provers can offer. A powerful proof technique, known as up to expansion, is discussed and applied in a case study about write invalidate cache coherence. This example is of interest, as the system is parameterized in the number of its components, and the bisimulation relation reflects the coherence of the caches with the main memory.

@InProceedings{Roeckl::2000,
  author = 	 {C. R\"ockl},
  title = 	 {Proving Write-Invalidate Cache-Coherence with
                  Bisimulations in {Isabelle/HOL}},
  booktitle = 	 {Proc. FBT'00},
  pages =	 {69--78},
  year =	 2000,
  editor =	 {J. Grabowski and S. Heimer},
  publisher =	 {Shaker}
}

[ps] [proof-scripts]
[RE00] On the Mechanized Verification of Infinite Systems.
C. Röckl and J. Esparza. In Proc. SFB 342 Final Colloquium, pages 31-52. Fakultät für Informatik, Technische Universität München, 2000.

Abstract: Observation equivalence is a well-known technique for proving that a concurrent system satisfies its specification. We report on our experience in the mechanization of observation equivalence proofs with the help of a general-purpose theorem prover. Several case-studies are considered, incluiding an sliding window and a cache-coherence protocol. In all cases the system has an infinite number of states, and sometimes also an arbitrarily large number of components. We show how compositionality and bisimulation-up-to techniques can be applied to reduce the size of the proofs.

@InProceedings{Roeckl::Esparza::2000,
  author = 	 {C. R\"ockl and J. Esparza},
  title = 	 {On the Mechanized Verification of Infinite Systems},
  booktitle = 	 {Proc. SFB 342 Final Colloquium},
  pages =	 {31--52},
  year =	 2000,
  editor =	 {A. Bode and T. Ludwig},
  series =	 {Technical Report},
  organization = {Technische Universit\"at M\"unchen}
}

[ps] [proof-scripts]

 

 

 Theses

[Roe96] Charakterisierung von Halbordnungssemantiken durch Beweissysteme (in German).
C. Röckl. M.Sc. Thesis, Fakultät für Informatik, Technische Universität München.

Abstract: Various forms of non-interleaving process semantics have been studied in the literature. In contrast to standard interleaving semantics they do not only consider the actions produced by processes but also local and/or causal aspects. In this work we study for CCS with a bisimulation-based preorder a generalized form of non-interleaving semantics that can be instantiated to well-known preorders and equivalences like local-cause equivalence, or global-cause equivalence. The thesis contains axiomatizations of both strong and weak preorders for finite processes.

@MastersThesis{Roeckl::1996,
  author = 	 {C. R\"ockl},
  title = 	 {Charakterisierung von Halbordnungssemantiken durch
                  Beweissysteme},
  school = 	 {Fakult\"at f\"ur Informatik,
                  Technische Universit\"at M\"unchen},
  year = 	 1996,
  note =	 {In German.}
}

[ps]
[Roe01a] On the Mechanized Validation of Infinite-State and Parameterized Reactive and Mobile Systems.
C. Röckl. Ph.D. Thesis, Fakultät für Informatik, Technische Universität München. TUM Online Publication (Link), 2001.

Abstract: The growing influence of telecommunication-systems in all areas has brought with it the need for elaborate and reliable software running on concurrent and, in particular, dynamically changing systems. With the development of such systems becoming ever more complex, the outline and development of mechanized and mechanizable verification-techniques is indispensable. This overall goal can be divided into three tasks: (1) outline of a framework in which (2) complex systems can be analysed, and the (3) design and implementation of efficient proof-techniques. It is certainly beyond the scope of a thesis to provide an integrated framework dealing with these questions within one environment. This work therefore concentrates on dominant aspects of each of the three tasks in separate discussions. A major result of the thesis is that the approaches outlined for each of the three questions obviously fit together, so that they can be used as a basis for the development of an integrated framework. Often automatic verification of larger hardware- and software-applications is impossible, because the systems are too large or even infinite. This thesis focusses on infinite-state and parameterized systems, and builds tool-support on interactive theorem-proving. Further, it concentrates on the validation of correct implementations by exploiting behavioural reasoning. It demonstrates how to apply various techniques to tackle proofs about infinite-state and parameterized systems with large descriptions, discusses the support that theorem-provers can offer, and presents a foundational platform for reasoning about mobile systems in a general-purpose theorem-prover.
Several design-decisions have to be taken. This thesis uses process-algebra as a framework, in particular CCS for the description and analysis of infinite-state reactive systems, and the pi-calculus for the discussion of mobile and higher-order systems. For a validation, it applies observation-equivalence, exploiting a range of proof-techniques that have been developed for the two calculi. For all mechanizations, the general-purpose theorem-prover Isabelle/HOL is used.

@PhdThesis{Roeckl::2001a,
  author = 	 {C. R\"ockl},
  title = 	 {On the Mechanized Validation of Infinite-State
                  and Parameterized Reactive and Mobile Systems},
  school = 	 {Fakult\"at f\"ur Informatik,
                  Technische Universit\"at M\"unchen},
  year = 	 2001
}

[ps] [errata] [proof-scripts]

 

 

 Reports

[Roe95] Proof Tableaux for Basic Parallel Processes.
C. Röckl. Technical Report, Fakultät für Informatik, Technische Universität München, 2001.

Abstract: Due to their constructiveness, recent proofs of the decidability of the strong bisimulation equivalence and the local cause equivalence of recursive BPP (Basic Parallel Processes) have provided algorithms based on the underlying tableau systems. The work in hand compares two just slightly distinct proof systems, the first of them testing on the strong bisimulation equivalence of BPP and the second testing on a more restricted notion of equivalence, the local cause equivalence. The latter is not merely a subclass of the former, but a proper one, for which a standard example will be given. Annotated to this work is a Scheme program executing both the proof utilising strong bisimulation and the one utilising local cause bisimulation upon BPP.

@TechReport{Roeckl::1995,
  author = 	 {C. R\"ockl},
  title = 	 {Proof Tableaux for Basic Parallel Processes},
  institution =  {Fakult\"at f\"ur Informatik,
                  Technische Universit\"at M\"unchen},
  year = 	 1995
}

[ps] [software]
[Roe97] How to make substitution preserve strong bisimilarity.
C. Röckl. Technical Report SFB 342/11/97, Fakultät für Informatik, Technische Universität München.

Abstract: We show that strong bisimilarity of CCS processes without summation and relabelling is preserved by any substition modulo the maintenance of internal channels, if the processes bear unique input locations. By this we understand a syntactic means of preventing that substitutions, which are in general not injective, cause synchronisation in one but not in the other of two originally bisimilar processes.

@TechReport{Roeckl::1997,
  author = 	 {C. R\"ockl},
  title = 	 {How to make substitution preserve strong bisimilarity},
  institution =  {Fakult\"at f\"ur Informatik,
                  Technische Universit\"at M\"unchen},
  year = 	 1997,
  number =	 {SFB 342/11/97}
}

[ps]
[OCRZ02] A Nominal Theory of Objects with Dependent Types
M. Odersky, V. Cremet, C. Röckl, M. Zenger. Technical Report IC/2002/070, 2002.

Abstract: We design and study newObj, a calculus and dependent type system for objects and classes which can have types as members. Type members can be aliases, abstract types, or new types. The type system can model the essential concepts of JavaBETA or gbeta. It can also model most concepts of SML-style module systems, including sharing constraints and higher-order functors, but excluding applicative functors. The type system can thus be used as a basis for unifying concepts that so far existed in parallel in advanced object systems and in module systems. The technical report presents results on confluence of the calculus, soundness of the type system, and undecidability of type checking.

@TechReport{Odersky::Cremet::Roeckl::Zenger::2002,
  author = 	 {M. Odersky and V. Cremet and C. R\"ockl and M. Zenger},
  title = 	 {A Nominal Theory of Objects with Dependent Types},
  institution =  {School of Computer and Communication Sciences,
                  Ecole Polytechnique F\'{e}d\'{e}rale de Lausanne},
  year = 	 2002,
  number =	 {IC/2002/070}
}

[pdf]