Journal Papers
[RH03] 
A Fully Adequate Shallow Embedding of the PiCalculus
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 higherorder abstract
syntax technique to generalpurpose theorem proving, yielding shallow
embeddings of the binders of formalized languages. Higherorder
abstract syntax has been applied with success in specialized logical
frameworks which satisfy a closedworld assumption. As more general
environments (like Isabelle/HOL or Coq) do not support this
closedworld assumption, higherorder 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 twolevel wellformedness
predicate, further preparing the ground for an implementation of
structural induction in terms of rule induction, and hence providing
fullyfledged syntax analysis. In order to apply and justify
wellformedness predicates, the paper develops a proof technique based
on a combination of instantiations and reabstractions of higherorder
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 picalculus 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 PiCalculus Process Semantics of Concurrent
Idealized ALGOL.
C. Röckl and
D.
Sangiorgi.
In Proc. FOSSACS'99,
LNCS 1578, pages 306321.
Springer, 1999.
Abstract:
We study the use of the picalculus 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
picalculus semantics. As behavioural equivalence on
picalculus 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 picalculus semantics is sound. This allows for applying the
picalculus 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 = {306321},
year = 1999,
editor = {W. Thomas},
volume = 1578,
series = {Lecture Notes in Computer Science},
publisher = {Springer}
}
[ps]

[RE99] 
ProofChecking Protocols Using Bisimulations.
C. Röckl and
J.
Esparza.
In Proc. CONCUR'99,
LNCS 1664, pages 525540.
Springer, 1999.
Abstract:
Observation equivalence is of particular interest to the
verification of concurrent systems, as it is compositional,
detects deadlocks, and possesses a welldeveloped theory. We
examine the mechanization of proofs by exhibiting bisimulation
relations. As examples we have chosen infinitestate, 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
valuepassing 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
builtin proof tactics.
@InProceedings{Roeckl::Esparza::1999,
author = {C. R\"ockl and J. Esparza},
title = {ProofChecking Protocols using Bisimulations},
booktitle = {Proc. CONCUR'99},
pages = {525540},
year = 1999,
editor = {J.C.M. Baeten and S. Mauw},
volume = 1664,
series = {Lecture Notes in Computer Science},
publisher = {Springer}
}
[ps]
[proofscripts]

[RHB01] 
HigherOrder Abstract Syntax with Induction in Isabelle/HOL:
Formalizing the PiCalculus and Mechanizing the Theory of
Contexts.
C. Röckl and
D.
Hirschkoff and
S.
Berghofer.
In Proc. FOSSACS'01,
LNCS 2030.
Springer, 2001.
Abstract:
Higherorder abstract syntax is a natural way to formalize
programming languages with binders, like the picalculus, because
alphaconversion, instantiations and capture avoidance are
delegated to the metalevel of the provers, making tedious
substitutions superfluous. However, such formalizations usually
lack structural induction, which makes syntaxanalysis
impossible. Moreover, when applied in logical frameworks with
objectlogics, 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 picalculus in
Isabelle/HOL, using wellformedness predicates which both
eliminate exotic terms and yield structural induction. These
inductionprinciples 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 = {HigherOrder Abstract Syntax with Induction
in {Isabelle/HOL}: Formalizing the PiCalculus and
Mechanizing the Theory of Contexts},
booktitle = {Proc. FOSSACS'01},
pages = {364378},
year = 2001,
editor = {F. Honsell and M. Miculan},
volume = {2030},
series = {Lecture Notes in Computer Science},
publisher = {Springer}
}
[ps]
[proofscripts]

[Roe01b] 
A FirstOrder Syntax for the PiCalculus in
Isabelle/HOL using Permutations.
C. Röckl.
In Proc. MERLIN'01,
ENTCS 58.1.
Elsevier,
2001.
Abstract:
A formalized theory of alphaconversion for the picalculus
in Isabelle/HOL is presented. Following a recent proposal
by Gabbay and Pitts, substitutions are modelled in terms of
permutations, and alphaequivalence 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 FirstOrder Syntax for the PiCalculus 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]
[proofscripts]

[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
SMLstyle module systems, including sharing constraints and
higherorder 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] 
FirstOrder Proofs for HigherOrder Languages.
C. Röckl.
In Proc. FBT'99, pages 193202.
Utz, 1999.
Abstract:
We study the use of the picalculus for semantical descriptions
of higherorder 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 firstorder environment, we encode
CIA in the picalculus, exploiting results that its mobility allows
a firstorder 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 = {FirstOrder Proofs for HigherOrder Languages},
booktitle = {Proc. FBT'99},
pages = {193202},
year = 1999,
editor = {B. Sch\"atz and K. Spies},
publisher = {Utz}
}
[ps]

[Roe00] 
Proving WriteInvalidate CacheCoherence with Bisimulations in
Isabelle/HOL.
C. Röckl.
In Proc. FBT'00, pages 6978.
Shaker, 1999.
Abstract:
The aim of this paper is to advocate the use of bisimulation
relations in the verification of infinitestate or parameterized
systems, and demonstrates the support that generalpurpose 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 WriteInvalidate CacheCoherence with
Bisimulations in {Isabelle/HOL}},
booktitle = {Proc. FBT'00},
pages = {6978},
year = 2000,
editor = {J. Grabowski and S. Heimer},
publisher = {Shaker}
}
[ps]
[proofscripts]

[RE00] 
On the Mechanized Verification of Infinite Systems.
C. Röckl and J. Esparza.
In Proc. SFB 342 Final Colloquium, pages 3152.
Fakultät für
Informatik,
Technische Universität
München, 2000.
Abstract:
Observation equivalence is a wellknown 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 generalpurpose theorem prover. Several casestudies are
considered, incluiding an sliding window and a cachecoherence 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 bisimulationupto 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 = {3152},
year = 2000,
editor = {A. Bode and T. Ludwig},
series = {Technical Report},
organization = {Technische Universit\"at M\"unchen}
}
[ps]
[proofscripts]

