Joachim Parrow, Short CV

Education and Employments

Born 25 Dec. 1956; Swedish Citizen, Married, three children. BSc in Computer Science, Uppsala University 1980; PhD in Computer Science, Uppsala University 1986 (Thesis title: Fairness properties in process algebra), Docent 1990.

Joachim Parrow is professor in Computing Systems (Datalogi) and head of division at the department of Information Technology at Uppsala University. From July 2017 -- June 2023 he was Dean of Mathematics and Computer Science. 2001--2010 he was professor of Computer Systems at the same department. 2005--2008 he was member of the faculty board and Dean of Education, and 2002--2005 he was Head of Education.

During 1994-2001 he was professor in Distributed Systems at the Department of Microelectronics and Information Technology at the Royal Institute of Technology (KTH), Stockholm. There he was a member of Centrala Tjänsteförslagsnämnden, the committee for promotions of lecturers to professors. From April 1997 until October 2000 he was Prefekt (Head of Department), and 1997-1999 a member of the Scientific Council of the School of Electrical Engineering and Information Technology at KTH.

During 1986-1994 he was employed as a researcher at the Swedish Institute of Computer Science, leading the research group on Formal Design Techniques.

During 1986-1989 he spent in all 18 months at the University of Edinburgh, working with Robin Milner.

Research Interests

Joachim Parrow works in the group on Theory for Mobile Processes . He has been working in the general area of formal methods for concurrent and distributed systems, mainly process algebraic formalisms and related logics and their applications in automated tools for formal verification. He began the development of the Concurrency Workbench (an automated verification tool for CCS) in 1986, and collaborated with Robin Milner and David Walker in developing the pi-calculus (a calculus of mobile processes) 1987-1989. Recent research has focussed on developing and applying the pi-calculus, notably in the Psi- calculi and in formalising calculi in the theorem prover Isabelle.

Joachim Parrow is an ISI highly cited researcher (2001).

Previous Students

Joachim Parrow has advised ten students to a PhD:
Peter Sjödin (Uppsala 1991),
Fredrik Orava (Uppsala 1994),
Björn Victor (Uppsala 1998),
Gunnar Övergaard (KTH 2000),
Jose Vivas (KTH 2001),
Lars-åke Fredlund (KTH 2001),
Oskar Wibling (Uppsala 2008),
Jesper Bengtson (Uppsala 2010),
Magnus Johansson (Uppsala 2010),
Johannes Åman Pohjola (Uppsala 2016).
and five to a Licentiat degree.

Service

Joachim Parrow was Programme Committee chair for ICALP track B 2003. He was Co-Chair for EXPRESS'97, Programme Committee Co-Chair for FTRTFT'96 and Programme Committee Chair for Concur'94, and co-chair for PSTV'91.

He was a member of the programme committees for CONCUR'90, PSTV'93, CONCUR'95, CAV'95, FTRTFT'98, CONCUR'98, ICALP'00, EXPRESS'01, CONCUR'02, ICALP'04, TGC'05, CONCUR'09, ICALP'11, FOSSACS'12, MeMo'14, MeMo'15, CONCUR'16.

He is an editor of Logical Methods in Computer Science. He has been guest editor of Information and Computation, Computer Networks and ISDN Systems and of Nordic Journal of Computing.

He was active in the formation of the NUTEK Comptence Center ASTEC 1994 and a member of its board until 1998. He was a member of the board of SICS 1999-2002.

Recent Teaching

Programmering, a yearly second year course (in Swedish) on Python and Java.
The Science and Technology students' pedagogical prize 2009 (motivation in Swedish).

Former Projects

PROFUN, on programming wireless networks, funded by the Swedish Foundation for Strategic Research. UPMARC, on programming multicore architectures, funded by the Swedish Research Council. A Framework for parallel programming specifications. Funded by the Swedish Research Council. Project leader for SICS basic research projects FDT (1987-1990) and CORRECT (1990-1993). Leader of the Swedish contributions to the Esprit Basic Research projects CONCUR, 1989-1992, CONCUR2 (1992-1995), CONFER (1992-1995), and the working group EXPRESS (1994-1996). Project leader of the TFR project High Level Constructs for Protocol Design (1992-1995), the NUTEK project Methods for Distributed System Design(1993-1995), the ASTEC project BOOM: Formal Specification of Object-Oriented Modelling Concepts (1995-1998) and the TFR "ramanslag" Semantics and Proofs for Programming Languages, 1999-2002. Co-ordinator of the EU IST/GC project PROFUNDIS (2002-2005).

Selected Papers

See also my DBLP page and my google scholar page. Warning: Links to journal papers below are not always verbatim copies. In most cases they are pretty close though. Note that copyrights for these have been transferred to the publishers.

Joachim Parrow, Johannes Borgström, Lars-Henrik Eriksson, Ramunas Gutkovas, and Tjark Weber. Modal Logics for Nominal Transition Systems, http://arxiv.org/abs/1904.02564 (2021).
Joachim Parrow, Tjark Weber, Johannes Borgström, Lars-Henrik Eriksson: Weak Nominal Modal Logic> Proceedings FORTE 2017:179-193 (2017).
Joachim Parrow and Tjark Weber. The Largest Respectful Function.LMCS vol 12 (2016).
Johannes Åman Pohjola and Joachim Parrow. Bisimulation Up-To Techniques for Psi-Calculi, CPP 2016:142-153.
Johannes Åman Pohjola and Joachim Parrow. The Expressive Power of Monotonic Parallel Composition, ESOP 2016:780-803.
Johannes Borgström, Ramunas Gutkovas, Joachim Parrow, Björn Victor, and Johannes Åman Pohjola. A Sorted Semantic Framework for Applied Process Calculi. LMCS 12(1) (2016)
Joachim Parrow, Johannes Borgström, Lars-Henrik Eriksson, Ramunas Gutkovas, and Tjark Weber. Modal Logics for Nominal Transition Systems, In Concur 2015:198-211 (2015)
Jesper Bengtson, Joachim Parrow, and Tjark Weber. Psi-calculi in Isabelle. Journal of Automated Reasoning 56(1) pp 1-47 (2015), http://link.springer.com/article/10.1007/s10817-015-9336-2.
Johannes Borgström, Shuqin Huang, Magnus Johansson, Palle Raabjerg, Björn Victor, Johannes Åman Pohjola, Joachim Parrow. Broadcast psi-calculi with an application to wireless protocols. Software and System Modeling 14(1): 201-216 (2015)
Virginia Grande and Joachim Parrow. Motivation and Grade Gap Related to Gender in a Programming Course. In Innovation and Technology in Computer Science Education 2015: 349.
Joachim Parrow. General Conditions for Full Abstraction. Math. Struct. in Comp. Science / 26:655-657, 2014
Johannes Åman Pohjola, Joachim Parrow. Priorities Without Priorities: Representing Preemption in Psi-Calculi. In EXPRESS/SOS 2014: 2-15
Johannes Borgström, Ramunas Gutkovas, Joachim Parrow, Björn Victor, and Johannes Åman Pohjola. A Sorted Semantic Framework for Applied Process Calculi. In Proc. Trustworthy Global Computing 2013, pp 103-118, LNCS 8358, 2014.
Magnus Johansson, Björn Victor, and Joachim Parrow. Computing strong and weak bisimulations for psi-calculi. J. Logic and Algebraic Programming, Available online 31 January 2012, ISSN 1567-8326, 10.1016/j.jlap.2012.01.001. (http://www.sciencedirect.com/science/article/pii/S1567832612000021) 2012.
Joachim Parrow, Johannes Borgström, Palle Raabjerg, Johannes Åman Pohjola. Higher-order psi-calculi. Math. Struct. in Comp. Science CJO 2013 doi:10.1017/S0960129513000170 , 2013.
Johannes Borgström, Shuqin Huang, Magnus Johansson, Palle Raabjerg, Björn Victor, Johannes Åman Pohjola, and Joachim Parrow. Broadcast Psi-calculi with an Application to Wireless Protocols. Accepted for publication in Software and System Modelling. A shorter version is in Software Engineering and Formal Methods: SEFM 2011, volume 7041 of Lecture Notes in Computer Science, pp 74-89, 2011.
Magnus Johansson, Jesper Bengtson, Joachim Parrow, and Björn Victor. Weak equivalences in psi-calculi. In Proceedings of LICS 2010 pages 322-331, IEEE Computer Society 2010.
Jesper Bengtson, Magnus Johansson, Joachim Parrow, and Björn Victor. Psi-calculi: A framework for mobile processes with nominal data and logic . Logical Methods in Computer Science 7(1:11) pp 1-44 (2011).
Magnus Johansson, Björn Victor, and Joachim Parrow. A fully abstract symbolic semantics for psi-calculi. In Proceedings of SOS'09, EPTCS vol. 18 pp 17-31 2010.
Jesper Bengtson and Joachim Parrow. Psi-calculi in Isabelle. In Berghofer et al (Eds), Proceedings of TPHOLs 2009, pages 99-114. Springer Verlag LNCS 5674 (2009).
Jesper Bengtson, Joachim Parrow. Formalising the pi-calculus using nominal logic. Logical Methods in Computer Science 5, 2:16, 2009. A shorter version is in H. Seidl (Ed) Proceedings of FOSSACS 2007, pages 63-77, Springer Verlag LNCS 4423 (2007).
Jesper Bengtson, Magnus Johansson, Joachim Parrow, and Björn Victor. Psi-calculi: Mobile processes, nominal data, and logic . In Proceedings of LICS 2009, pages 39-48. IEEE Computer Society (2009).
Magnus Johansson, Joachim Parrow, Björn Victor, and Jesper Bengtson. Extended pi-calculi. Proceedings of ICALP 2008 LNCS 5126 pp 87--98, Springer 2008. Note this erratum.
Jesper Bengtson, Joachim Parrow. A completeness proof for bisimulation in the pi-calculus using Isabelle. Presented att SOS 2007, Electronic Notes in Theoretical Computer Science 192:1, pages 61-75 .
Joachim Parrow. Expressiveness of Process Algebras. Electronic Notes in Theoretical Computer Science 209, pages 173-186 (2008) (draft presented at the LIX Colloquium on Emerging Trends in Concurrency Theory 2006).
Oskar Wibling, Joachim Parrow, Arnold Pears. Ad hoc routing protocol verification through broadcast abstraction. In F. Wang (Ed), Proceedings of FORTE 2005, pages 128-142. Published as Springer Verlag LNCS 3731 (2005).
Michael Baldamus, Joachim Parrow, Björn Victor. A fully abstract encoding of the pi-calculus with data terms. In L. Caires et al (Eds), Proceedings of ICALP 2005, pages 1202-1213. Published as Springer Verlag LNCS 3580 (2005).
Michael Baldamus, Joachim Parrow, Björn Victor. The spi-calculus translated to pi-calculus preserving may-tests. In H. Ganzinger (Ed), Proceedings of LICS 2004, pages 22-31. IEEE Computer Society Press (2004).
Oskar Wibling, Joachim Parrow, Arnold Pears. Automatized verification of ad hoc routing protocols. In D. de Frutos, M. Nunez (Eds), Proceedings of FORTE 2004, pages 343-358. Published as Springer Verlag LNCS 3235 (2004).
Cosimo Laneve, Joachim Parrow, Björn Victor. Solo diagrams. In N. Kobayashi and B.C. Pierce (Eds), Proceedings of TACS 2001 pages 127-144, Published as Springer Verlag LNCS 2215 (2001).
Joachim Parrow. An Introduction to the pi-Calculus. In Handbook of Process Algebra, ed. Bergstra, Ponse, Smolka, pages 479-543, Elsevier (2001)
Joachim Parrow. Trios in Concert. In Proof, Language and Interaction, Essays in Honour of Robin Milner, ed. Plotkin, Stirling, Tofte, pages 621-637, MIT Press (2000).
Joachim Parrow. On the relationship between two proof systems for the pi-calculus. Pi-calculus note JP15 (1999). [plain text]
Joachim Parrow, Björn Victor. The Tau-laws of Fusion. In D. Sangiorgi and R. de Simone, eds, Proceedings of CONCUR'98, LNCS 1466, pages 99-114. Springer-Verlag (1998).
Joachim Parrow. Programmeraren som Schaman. Forskning och Framsteg 2/98:14-19 (1998). [In Swedish, html format]
Björn Victor, Joachim Parrow. Concurrent Constraints in the Fusion Calculus. In K.G. Larsen, S. Skyum and G. Winskel, eds, Proceedings of ICALP'98, LNCS 1443, pages 455-469. Springer-Verlag (1998).
Joachim Parrow, Björn Victor. The Fusion Calculus. In the Proceedings of LICS'98, pages 176-185, IEEE Computer Society Press (1998). [61KB] (The long version here incudes proofs)
Joachim Parrow. Trollkarlen blir Ingenjör - Formella Metoder: En Översikt. In Swedish (1997).
Joachim Parrow, Björn Victor. The Update Calculus. In M. Johnson, ed, Proceedings of AMAST'97, volume 1349 of LNCS, pages 409-423. Springer-Verlag (1997).
Björn Victor, Joachim Parrow. Constraints as Processes. In U. Montanari & V. Sassone, eds, Proceedings of CONCUR'96, volume 1119 of LNCS, pages 389-405. Springer-Verlag (1996).
Joachim Parrow, Peter Sjödin. Designing a Multiway Synchronisation Protocol. Computer Communications 19:1151-1160 (1996).
Joachim Parrow. Trollkarlens Hatt. In Mellan Himmel och Jord, KTH (1995). Paper presented at my inauguration, in Swedish [Without pictures]. The HTML version includes pictures!
Joachim Parrow. Interaction Diagrams. Nordic Journal of Computing 2:407-443 (1995)
Joachim Parrow, Davide Sangiorgi. Algebraic Theories of Name-Passing Calculi. Information and Computation 120(2):174-197 (1995)
Joachim Parrow, Peter Sjödin. The Complete Axiomatization of Cs-Congruence. In Enjalbert, Mayr and Wagner (Eds): 11th Annual Symposium on Theoretical Aspects of Computer Science, Caen, France, Feb. 1994, pages 557-568. Published as Springer Verlag LNCS 775 (1994)
Rance Cleaveland, Joachim Parrow, Bernhard Steffen. The Concurrency Workbench: A Semantics Based Tool for the Verification of Concurrent Systems. ACM Transactions on Programming Languages and Systems 15:36-72 (1993).
Bengt Jonsson, Joachim Parrow. Deciding Bisimulation Equivalences for a Class of Non-Finite-State Programs. Information and Computation107:272-302 (1993).
Robin Milner, Joachim Parrow, David Walker. Modal Logics for Mobile Processes. Theoretical Computer Science 114:149-171 (1993).
Joachim Parrow. Structural and Behavioural Equivalences of Networks. Information and Computation 107:58-90 (1993).
Robin Milner, Joachim Parrow, David Walker. A Calculus of Mobile Processes - Part I and Part II. Information and Computation 100:1-77 (1992).
Fredrik Orava, Joachim Parrow. An Algebraic Verification of a Mobile Network. Formal Aspects of Computing 4:497-543 (1992). [Two figures missing. The two figures are here, ]
Joachim Parrow, Peter Sjödin. Multiway Synchronization Verified with Coupled Simulation. In Cleaveland (Ed): Proceedings of CONCUR '92 , Stony Brook, NY, August 1992, pages 518-533. Published as Springer Verlag LNCS 630 (1992).
Joachim Parrow. The Expressive Power of Parallelism. Future Generation Computer Systems 6:271-285 (1990).
Lars-åke Fredlund, Bengt Jonsson, Joachim Parrow. An Implementation of a Transitional Semantics for an Imperative Language. In Baeten, Klop (Eds): Proceedings of CONCUR '90, Amsterdam, August 1990, pages 246-262. Published as Springer Verlag LNCS 458 (1990).
Joachim Parrow. Submodule Construction as Equation Solving in CCS. Theoretical Computer Science 68:175-202 (1989). [No Figures]
Joachim Parrow. Verifying a CSMA/CD-Protocol with CCS. In Aggarwal, Sabnani (Eds): Proceedings of the 8th IFIP Symposium on Protocol Specification, Testing and Verification , June 1988, pages 373-384. North-Holland (1988).

Back to Joachim Parrow Home Page