|
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]
|
|
