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

 

Christine Röckl

Post-Doctoral Researcher
(Assistante)

LAMP - DI - EPFL
INR 320 (Ecublens)
CH-1015 Lausanne
Switzerland / Suisse

 

 

 Research Interests

So far I've mainly been into process-calculi, mobility, and theorem-proving. My latest project deals with a formalization of the pi-calculus in Isabelle/HOL using higher-order abstract syntax. You can find more about it here and on my old web-page.

I am currently trying to dig a little bit into the business of type-systems for object-oriented programming-languages. However this doesn't necessarily mean that I'm going to give up process-calculi completely.

 

 Bibliography

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

 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, bibtex] [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, bibtex] [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, bibtex] [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, bibtex] [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, bibtex] [pdf]

 Workshop Papers
[Roe99] First-Order Proofs for Higher-Order Languages.
C. Röckl. In Proc. FBT'99, pages 193-202. Utz, 1999.
[abstract, bibtex] [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, bibtex] [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, bibtex] [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, bibtex] [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, bibtex] [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, bibtex] [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, bibtex] [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, bibtex] [pdf]