Iris Workshop 2022

The second edition of the Iris workshop will be held in Nijmegen and it will be focused on Iris-related research to allow for in-depth talks and discussions. There will be a two-day long program with talks on Monday 2 May and Tuesday 3 May. Participants are encouraged to stay 1-3 days longer if they can, for more informal discussions and interaction.

Invited talks

• Aïna Linn Georges (Aarhus University, Denmark): Efficient Temporal Stack Safety on Capability Machines using Directed Capabilities
• Aymeric Fromherz (Inria, France): Steel, a Concurrent Separation Logic for F*
• Emanuele D'Osualdo (MPI-SWS, Germany): TaDA Live: Compositional Reasoning for Termination of Fine-grained Concurrent Programs
• Ike Mulder (Radboud University Nijmegen, The Netherlands): Automating your Iris proofs with Diaframe
• Koen Jacobs (KU Leuven, Belgium): Purity of an ST Monad: Full Abstraction by Semantically Typed Back-Translation

Program

Monday 2 May

• 08:30 - 09:00: Coffee
• 09:00 - 09:30: Jonas Kastberg Hinrichsen (Aarhus University, Denmark): The Actris Ghost Theory: Session Type-Based Ghost Theory for Reasoning about Reliable Communication [abstract] [slides]
  Binary sessions, specifying bidirectional exchanges of messages between two processes, has widely been used to model idealised reliable communication, where messages are never dropped, duplicated, or arrive out of order. Such sessions allow for sophisticated protocol structures, as evidenced by the ever expanding work on session types, a behavioural type system for specifying the types of individual messages of a sequence of exchanges.
  However, the expressivity of these session types is often restricted to a decidable fragment, which limits their capabilities for reasoning about functional correctness. Furthermore, the session types literature primarily considers the idealised setting, which does not account for more complex reliable communication layers, e.g. with message duplication alongside duplicate-protection.
  In this talk, I will cover the ongoing story of Actris, a framework for session type-based reasoning in separation logic, and how it can be used to reason about reliable communication in arbitrary settings. In particular, I will elaborate on a generic process of applying the ghost theory of Actris to obtain reliable communication primitives for systems with an arbitrary communication layer. To this effect, I provide a concrete instantiation of the Actris ghost theory for node-local reliable channels in an ML-like language.
• 09:30 - 10:00: Léon Gondelman (Aarhus University, Denmark): Tying Loose Ends: Modular Verification of Client-Server Communication using Distributed Separation Logic and Dependent Separation Protocols [abstract] [slides]
  In the past few years, Iris has been successfully applied to achieve modular verification of communicating processes in two different directions. On one side, the Actris project introduced binary session protocols as a high-level specification pattern to reason about connected reliable binary communication but has applied it to reason about message-passing concurrency, where the communication layer itself is reliable. On the other side, Aneris project enabled reasoning about realistic distributed programs, which communicate over an unreliable UDP-like network. This can suit reasoning about programs for which connected or reliable communication is not needed but requires to set up mechanisms such as retransmission/acknowledgments and sequence numbering of messages every time the session guarantees (in-order message delivery without duplicates) are needed.
  Together with Jonas Kastberg Hinrichsen we have recently let Aneris and Actris projects meet to enable reasoning about reliable communication in distributed systems. The rendez-vous point is our verified library that provides BSD socket-like API primitives (connect, listen, accept, send, recv) for client-server reliable communication which we have implemented in OCaml. Our implementation is then automatically translated into Aneris, where it is verified in a highly modular way: (a) the four-way handshake initialization and the retransmission/acknowledgments mechanisms are verified using all of Aneris facilities to reason about node-local concurrency and networking; (b) the data exchange send and receive operations exposed to the user by the API are verified using session dependent protocols of Actris (c) to verify clients against our library one need only use the specified API, which carries away internal details of the concrete proof.
  Our work provides hence a piece of additional evidence that Actris Ghost Theory represents a general domain-independent framework for reliable communication and allows using Aneris to reason both about client-server reliable communication and unreliable unconnected communication within the same framework. In this talk, I will cover some of the key aspects and interesting points of our work and explain how this modularity has been achieved.
• 10:00 - 10:30: Jules Jacobs (Radboud University Nijmegen, The Netherlands): Connectivity Graphs: A Method for Proving Deadlock Freedom Based on Separation Logic [abstract] [slides]
  Linear types can be used to guarantee memory leak freedom, and also to guarantee deadlock freedom (e.g. with session types). Proving such properties formally in Coq is made challenging because this relies on reasoning about the acyclicity of the connectivity graph structure between threads and the communication channels that connect them. We introduce a generic connectivity graph framework to encapsulate the reasoning about such graph structure away from the language-specific reasoning about typing. This framework can be used to prove deadlock and memory leak freedom in the style of progress and preservation and uses separation logic as a meta theoretic tool to treat connectivity graph edges and labels substructurally. To prove preservation locally, we distill generic separation logic rules for local graph transformations that preserve acyclicity of the connectivity graph. To prove global progress locally, we introduce a waiting induction principle for acyclic connectivity graphs. We use the framework to give mechanized proofs of deadlock and memory leak freedom for a variant GV (a session typed functional language), MPGV (a new variant of GV featuring multiparty session types), and μGV (a new minimalist concurrent lambda calculus). In the future, we would like to investigate whether connectivity graphs can also be used to create an Iris-based program logic that ensures deadlock freedom.
• 10:30 - 11:00: Coffee break
• 11:00 - 12:00: Aymeric Fromherz (Inria, France): Steel, a Concurrent Separation Logic for F* [abstract]
  F* is a proof-oriented programming language with support for dependent types and user-defined effects, which has been used to develop several sequential real-world applications, such as the HACL*/EverCrypt cryptographic provider and the EverParse library of verified parsers and serializers. In this talk, we present Steel, a framework based on concurrent separation logic that extends F* with support for concurrency. Steel draws inspiration from Iris and provides a highly expressive, impredicative separation logic with support for partial commutative monoids and dynamically allocated invariants. However, while Iris provides a powerful logical framework into which other logics and programming languages can be embedded, Steel instead aims to extend an existing proof assistant's language and reasoning facilities, leading to several design decisions that distinguish it from Iris.
  In this talk, we will give a tour of Steel, and emphasize on the significant points of contrast with Iris. In particular, we will present how we shallowly embed a concurrent separation logic into F*, and provide a high level of proof automation through a cooperation between the Z3 SMT solver and custom decision procedures implemented as F* tactics. We will finally demonstrate the programmability of Steel by presenting the implementation and verification of several libraries that illustrate key features of the framework.
• 12:00 - 12:30: Michael Sammler (MPI-SWS, Germany): Predictable, efficient, and extensible Iris automation with Lithium [abstract] [slides] [coq demo]
  This talk presents the Lithium proof automation for Iris that has been used to automate a refinement and ownership type system for C (RefinedC) and a separation logic for a realistic model of Arm and RISC-V assembly (Islaris). Even though these applications are quite complex, the core Lithium proof automation is based on a simple principle that everyone using Coq is familiar with: goal-directed proof search without backtracking. This talk shows how proof automation via goal-directed proof search can be applied to Iris and how it results in a predictable, efficient, and extensible proof automation for Iris. This talk will be structured as an interactive demonstration of Lithium in Coq.
• 12:30 - 14:00: Lunch
• 14:00 - 15:00: Ike Mulder (Radboud University Nijmegen, The Netherlands): Automating your Iris proofs with Diaframe [abstract] [slides]
  Proofs in Iris often contain steps that are 'obvious' for humans, yet difficult for automation. Think of closing invariants, instantiating existentials, and mutating ghost state. Existing tools like eauto and iFrame are not always able to handle such cases. In this talk, I will demonstrate Diaframe: a plugin for Iris that offers strong, extensible proof automation. Inspired by ideas from logic programming and bi-abduction, Diaframe can open and close invariants when appropriate, perform ghost updates automatically, and can easily be mixed with existing interactive proofs. I will walk you through the process of extending Diaframe for different programming languages and resources, and discuss some of the limitations and open problems.
• 15:00 - 15:30: Steven Keuchel (Vrije Universiteit Brussels, Belgium): Verified Symbolic Execution with Kripke Specification Monads (and no Meta-Programming) [abstract] [slides]
  Verifying soundness of symbolic execution-based program verifiers is a significant challenge. This is especially true if the resulting tool needs to be usable outside of the proof assistant, in which case we cannot rely on shallowly embedded assertion logics and meta-programming. The tool needs to manipulate deeply embedded assertions, and it is crucial for efficiency to eagerly prune unreachable paths and simplify intermediate assertions in a way that can be justified towards the soundness proof. Only a few such tools exist in the literature, and their soundness proofs are intricate and hard to generalize or reuse. We contribute a novel, systematic approach for the construction and soundness proof of such a symbolic execution-based verifier. We first implement a verification condition generator as an object language interpreter in a specification monad, using an abstract interface featuring angelic and demonic nondeterminism. Next, we build a symbolic executor by implementing a similar interpreter, in a symbolic specification monad. This symbolic monad lives in a universe that is Kripke-indexed by variables in scope and a path condition. Finally, we relate the resulting symbolic executor with the concrete verification condition generator using a Kripke logical relation. We report on the practical application of these techniques in Katamaran, a tool for verifying security guarantees offered by instruction set architectures (ISAs). The tool is fully verified by combining our symbolic execution machinery with a soundness proof of the concrete verification conditions against an axiomatized separation logic, and an Iris-based implementation of the axioms, proven sound against the operational semantics. Based on our experience with Katamaran, we can report good results on practicality and efficiency of the tool, demonstrating practical viability of our symbolic execution approach.
• 15:30 - 16:00: Coffee break
• 16:00 - 16:30: Zongyuan Liu (Aarhus University, Denmark): A Separation Logic for Communicating Virtual Machines [abstract] [slides]
  A hypervisor is a piece of software that allows one host machine to support mutiple guest virtual machines (VMs). Hypervisors are used extensively for virtualization in cloud computing and more. A hypervisor ensures that each VM runs as if on bare metal, and at the same time pro- vides isolation, to separate untrusted code from security-critical code. We study the Hafnium hypervisor initially developed at Google. Hafnium implements hypercalls for communication among VMs, both via memory sharing and via message passing, following the FF-A specification of ARM, and Hafnium is claimed to provide memory isolation for those parts of the memory that are not shared via communication. We present an operational semantics which models the essential behavior of Hafnium, with fairly realistic hypercall interfaces. We further develop a program logic for modular formal verification of client VM programs that can communicate with other VMs via hypercalls, and a logical relation that captures the extent to which unknown code running on a VM is isolated from other VMs. Using the program logic and the logical relation, we reason about known VM programs that interact with VMs running arbitrary unknown code, and show robust safety: no matter what the unknown code does, it cannot violate specifications proved for the known code. This captures key aspects of the desired memory isolation properties of the hypervisor. All of the work has been mechanized using the Iris separation logic framework in Coq.
  Joint work with Sergei Stepanenko, Aslan Askarov, Jean Pichon-Pharabod, Amin Timany, Lars Birkedal.
• 16:30 - 17:00: Paolo G. Giarrusso (Bedrock Systems, Germany): Programming a Microkernel Specification in Separation Logic [abstract] [slides]
  Microkernel specifications must support reasoning about well-behaved clients in the presence of untrusted code. To this end, one can give an operational model of the abstract machine offered by the operating system; but it is challenging to build a faithful large-footprint operational model for a realistic microkernel using fine-grained concurrency, which will expose non-deterministic behavior and non-atomic sequences of atomic steps.
  To address this problem, we give our microkernel specifications operational-like specifications directly in separation logic, similarly to what is done in TaDA. This way, we can use existential quantification to model non-deterministic choice, iterated atomic updates to express sequencing, and separating conjunction to model (a slightly relaxed form of) non-deterministic evaluation order that we have found suitable in practice. We apply these techniques to our specification of NOVA, the L4-family microkernel that forms the foundation of the BedRock HyperVisor.
  On top of these specifications, we can both derive pleasant reasoning principles for well-behaved code, and (according to a proof sketch) we can verify software in the presence of unverified code.
  Joint work with Paolo G. Giarrusso, Gregory Malecha, David Swasey, Yoichi Hirai.
• 17:00 - 17:30: Hai Dang (Bedrock Systems, Germany): More hidden states, more modalities, and generalized invariants and ghost ownership [abstract] [slides]
  Local states are commonly used to maintain agreement within a component and isolation across components. A language level thread can has its own thread-local storage; a hypervisor maintains separate address spaces (virtual address translations) for its virtual machines; a processor has multiple-level caches that are local to a CPU core or a group of CPU cores. Reasoning about local states needs to make sure that (1) within a component, the local state is ambient, i.e. it is always readily available, but is unobtrusive to the reasoning and (2) across components, local states should be isolated, but can also be used in cross-component communications in a safe and secure way.
  Iris provides an abstraction called “monotone predicates” (monPred) to account for local states in form of "BI indices”, which was inspired by several weak memory developments in Iris. At BedRock Systems, we aim to handle, within a single logic, different types of local states at different levels of abstraction. This means that we also need to handle the composition, the interaction, and/or the abstraction between different types of local states. To that end, we develop “monotone lenses” to support the interaction between types of local states, and generalize monPred with monotone lenses, resulting in multiple local-state "modalities" inspired by the weak memory works. Furthermore, we push for the generalization of Iris invariants and ghost ownership for monPred with lenses.

Tuesday 3 May

• 08:30 - 09:00: Coffee
• 09:00 - 10:00: Koen Jacobs (KU Leuven, Belgium): Purity of an ST Monad: Full Abstraction by Semantically Typed Back-Translation [abstract] [slides]
  In 1995, Launchbury and Peyton Jones extended Haskell with an ST monad that allows the programmer to use higher-order mutable state. They informally argued that these state computations were safely encapsulated, and as such, that the rich reasoning principles stemming from the *purity* of the language, were not threatened.
  In this talk, we give a formal account of the preservation of *purity* after adding an ST monad to a simply-typed call-by-value recursive lambda calculus. We state and prove full abstraction when embedding the pure language into its extension with ST; contextual equivalences from the pure language continue to hold in the presence of ST.
  Proving full abstraction of compilers is usually done by emulating or *back-translating* the target features (here: ST computations) into the source language, a well-known challenge in the secure compilation community. We employ a novel proof technique for proving our full abstraction result that allows us to use a semantically (but not syntactically) typed back-translation into an intermediate language.
  In this talk, we'll spend some time on this proof technique. Specifically, we'll go over the intermediate semantically-typed language which is defined by logical relations expressed in the Iris framework and sketch out why a semantically typed back-translation is indeed sufficient. As mentioned, we'll apply the technique to back-translate ST computations. Lastly, we'll contemplate a bit about what the proof technique may entail more generally.
• 10:00 - 10:30: Xiaojia Rao (Imperial College London, UK): Iris Wasm: A Program Logic for WebAssembly [abstract] [slides]
  WebAssembly (Wasm) is a modern bytecode language, primarily designed to be a compilation target for other languages to run in browsers efficiently. The WebAssembly standard is described informal semantics, with several mechanised specifications including our work on WasmCert-Coq. In this talk, we describe Iris Wasm, a higher-order program logic for Wasm which builds on WasmCert-Coq and our previous first-order program logic for Wasm.
  Unlike ML-like languages (for example, HeapLang) which have been well-studied in Iris, Wasm is a stack-based language with complex control-flow instructions. Some of the common designs and techniques in Iris for reasoning about program behaviour are therefore not appropriate for Wasm. Iris Wasm therefore builds on Wasm directly, instead of working with an encoding of Wasm in a functional language. We will compare Iris reasoning for WebAssembly and HeapLang, highlighting the interesting differences. We will also demonstrate reasoning in Iris Wasm with some simple examples.
• 10:30 - 11:00: Coffee break
• 11:00 - 12:00: Aïna Linn Georges (Aarhus University, Denmark): Efficient Temporal Stack Safety on Capability Machines using Directed Capabilities [abstract] [slides]
  Capability machines are a type of CPUs that support fine-grained privilege separation using capabilities, machine words that include forms of authority. Formal models of capability machines and associated calling conventions have so far focused on establishing two forms of stack safety properties, namely local state encapsulation and well-bracketed control flow. In this joint work with Alix Trieu and Lars Birkedal, we present a novel kind of directed capability and show how to use them to make an earlier suggested calling convention more efficient. We define unary and binary logical relations, expressive enough to reason about temporal stack safety (in addition to local state encapsulation and well-bracketed control flow), and use them to verify concrete examples, all mechanised in Iris.
• 12:00 - 12:30: Simon Friis Vindum (Aarhus University, Denmark): A Concurrent Separation Logic for Weak Persistent Memory [abstract] [slides]
  In this talk, I will present a concurrent separation logic capable of verifying programs that make use of weak persistent memory. Persistent memory (also known as non-volatile memory) is a recently developed memory technology that promises to revolutionize the traditional storage hierarchy by combining the speed of DRAM with the durability of SDD/HDD. This makes it possible to forego secondary storage and store data permanently in memory — thus avoiding the complexity and overhead of serializing data to slower, but durable, secondary storage. The CPU’s caches are however expected to remain volatile. This means that data can not be written atomically to the persistent memory. Only a weak ordering on the order in which writes reach persistent memory is known. This makes reasoning about programs that makes use of persistent memory challenging, which is further complicated by the fact that the content of the persistent memory should always be recoverable after a crash.
• 12:30 - 14:00: Lunch
• 14:00 - 15:00: Emanuele D'Osualdo (MPI-SWS, Germany): TaDA Live: Compositional Reasoning for Termination of Fine-grained Concurrent Programs [abstract] [slides]
  Modern concurrent separation logics achieved great compositionality for proofs of partial correctness of fine-grained shared-memory concurrent programs. We have comparatively little understanding of compositional reasoning about progress (liveness) properties: that is, something good eventually happens (e.g. termination, deadlock-freedom). Yet, the intricacies of the design of concurrent programs often arise precisely from the need to guarantee progress properties.
  We introduce TaDA Live, a compositional separation logic for reasoning about the termination of fine-grained concurrent programs. In this talk, we will explain the design of TaDA Live total specifications and verification through examples. We will demonstrate that our specifications are expressive, concise, abstract, and atomic. To show they are also useful, we will give an overview of the verification system that uses these specifications. The proof system achieves compositionality by introducing a number of innovations: ghost state for liveness, modular deadlock detection and thread-local liveness reasoning.
• 15:00 - 15:30: Simon Oddershede Gregersen (Aarhus University, Denmark): Trillium: History-Sensitive Refinement in Separation Logic [abstract] [slides]
  Formal verification systems such as TLA+ have been widely used to design, model, and verify complex concurrent and distributed systems. In many of these tool suites, systems are modeled as state transition systems, and both safety and liveness properties can usually be checked. This enables users to reason about abstract system specifications and uncover design flaws, but it offers no guarantees about the implementations of systems nor about the relation between an implementation and its abstract specification.
  In this work, we show how to connect concrete implementations of concurrent and distributed systems to abstract system models. We develop Trillium, a language-agnostic separation logic framework for establishing history-sensitive refinement relations between programs and models. We use our logic to prove correctness of concrete implementations of two-phase commit and single-decree Paxos by showing that they refine their abstract TLA+ specifications. We further use our notion of refinement to transfer fairness assumptions on program executions to model traces and then transfer liveness properties of fair model traces back to program executions. This enables us to prove liveness properties such as strong eventual consistency of a concrete implementation of a Conflict-Free Replicated Data Type and fair termination of a concurrent program.
• 15:30 - 16:00: Coffee break
• 16:00 - 16:30: Simon Spies (MPI-SWS, Germany): Later Credits: Resourceful Reasoning for the Later Modality [abstract] [slides]
  Iris integrates two major lines of semantics and verification research: separation logic and step-indexed logical relations. The symbiosis of both enables powerful reasoning principles for (among other things) modelling richly typed languages like Rust. To incorporate step-indexed logical relations, propositions are given meaning through a step-indexed model in Iris, and step-indexed reasoning is reflected into the logic through the so-called "later" modality. As users of Iris know well, this modality is a blessing and a curse. On the one hand, it provides an elegant, high-level account of step-indexed reasoning. On the other hand, when used in sufficiently sophisticated ways, it can become a nuisance, turning perfectly natural proof strategies into dead ends.
  In this talk, I will present our recent work on later credits, a new technique for escaping later-modality quagmires. By leveraging the second ancestor of Iris—separation logic—later credits turn "the right to eliminate a later" into an ownable resource, which is subject to all the traditional modular reasoning principles of separation logic. Later credits enable new kinds of nontrivial step-indexed arguments, and also simplify existing proofs (e.g., by removing make-laterable from logical atomicity and by admitting an invariant opening rule without laters).
• 16:30 - 17:00: Glen Mével (Inria, France): Debits in nested suspensions: proof of Okasaki's banker's queue [abstract] [slides]
  By avoiding to compute the same thing twice, thunks are handy for implementing persistent data structures with good amortized time costs, regardless of their usage scenario. Okasaki's "banker's queue" is one such data structure; it uses a lazy list.
  Some program logics enable formal proofs of amortized time complexity by means of a resource called "time credits". In an earlier work, we have shown how to construct time credits within Iris, thus enabling time reasoning in a general-purpose program logic with separation. We have demonstrated this by proving a specification for a library of thunks, following Danielsson (2008). A thunk predicate has a time debit to be paid before the thunk can be forced. However, our previous work did not support anticipating debit from a nested thunk in an enclosing thunk; we need this reasoning rule to prove the banker's queue. Thus, we present an updated API and proof for thunks, and we sketch a proof of the correctness and amortized time complexity of the banker's queue.
• 17:00 - 17:30: Abel Nieto (Aarhus University, Denmark): Modular Verification of Commutative Replicated Datatypes in Separation Logic [abstract] [slides]
  Commutative Replicated Data Types (CRDTs) are a family of distributed data structures where all operations are designed to commute, so that replica states eventually converge. Additionally, CRDTs require that operations be propagated between replicas in causal order. This talk presents a framework for verifying safety properties of OCaml CRDT implementations using separation logic. The framework consists of two libraries. One implements a Reliable Causal Broadcast (RCB) protocol so that replicas can exchange messages in causal order. A second OpLib library then uses RCB to export a CRDT builder interface that simplifies the creation (and correctness proofs) of new CRDTs. OpLib allows clients to implement new CRDTs as purely-functional data structures, without having to reason about network operations, concurrency control and mutable state, and without having to re-implement causal broadcast each time. Using OpLib, we have implemented 10 sample CRDTs from the literature, including multiple versions of replicated registers and sets, as well as two CRDT combinators for products and maps. Our proofs are conducted in the Aneris distributed separation logic.

Location

The workshop will take place at Institute for Computing and Information Sciences
Mercator I building [map]
Toernooiveld 212, 6525 EC Nijmegen

The workshop will take place in room M0.28, on the ground floor of the Mercator I building.

The conference dinner will be in Nijmegen on Tuesday 3 May in The Pelgrim Foodbar, Franseplaats 1, Nijmegen [map].

Organizers

• Robbert Krebbers (Radboud University Nijmegen, The Netherlands)
• Amin Timany (Aarhus University, Denmark)
• François Pottier (Inria, France)

Registration

• Registration is free, but you should register online here.
• The early registration deadline is 8 April.
• Late registrations are possible until 22 April, but for late registrations we cannot guarantee a dinner spot due to necessary restaurant reservations.

This workshop is supported in part by the Dutch Research Council (NWO), project 016.Veni.192.259.

Practical information

Covid information

For traveling to the Netherlands. As of March 23, travelers coming from within the EU or the Schengen area will no longer be subject to test/vaccination/recovery requirements (there are still other requirements, like filling out a health declaration form if you travel by air). There are restrictions when traveling from other countries, read the information from the Dutch government and your own government/Dutch embassy in your country.

For inside the Netherlands. The Dutch government has dropped most restrictions inside the Netherlands. Read the information from the Dutch government for details. In particular, there are no vaccination/testing/mask restrictions for meetings and for visiting restaurants. As of March 23, masks are only mandatory at airports (you are of course welcome to wear a mask at other locations like the university or public transport). It is strongly recommend to take a self-test if you have symptoms, and to self-isolate if you test positive.

All Covid information is subject to change.

Travel by airplane to Nijmegen

Convenient airports are:

• Amsterdam Airport Schiphol (AMS). There is a direct train from Schiphol to Nijmegen that takes about 1:30 hour.
• Eindhoven Airport (EIN). It takes a bus trip of about 20 minutes to Eindhoven railway station. From there it takes 1:00 hour hour by train to Nijmegen.

There are also nearby airports in Germany: Dusseldorf airport (DUS) and Weeze Airport (NRN, also called Flughafen Niederrhein or Dusseldorf-Weeze Airport; not to be confused with DUS). There are trains from DUS to Nijmegen (they take 2:00-3:00 hour and require a number of switches). NRN has bad public transportation to Nijmegen.

If you travel by air, make sure to fill out the health declaration form.

Travel by train to Nijmegen

The Netherlands is well connected to the European train network. There are frequent international trains from among others UK (London), Germany, Belgium, and France to the Netherlands (it requires switching to a regional train to Nijmegen). You can plan your route at NS International.

Accommodation in Nijmegen

The best deals for hotels are typically found online with one of the many booking sites. Some possibilities:

• Mercure (Direct next to the station.)
• Van der Valk Lent (Outside the city center, but next to a railway station; the city center will be a 30-minute walk.)
• Guesthouse Vertoef
• Hotel Apollo
• Hotel Pauw
• Hotel Credible

Traveling from the Nijmegen city center to the university

It is a 30-minute walk from the city center to the Mercator building.

• The most Dutch way to travel around in the city is by bike. Rental bikes are available at the main railway station and at Jasper fietsen.
• By train you can reach the university with a 3-minute ride from Nijmegen to Nijmegen Heyendaal (and an additional 5-minute walk). There is a train every 15 minutes during the daytime. In the evening there is a train every 30 minutes.
• There are frequent buses from the railway station to the campus. During rush hour bus line 10, the Heyendaal Shuttle, runs every five minutes directly from the central station to the campus. Note that buses stop only on request. Use the 9292 journey planner or Google maps for all bus/train planning.
• There is paid parking at the university.

For traveling by bus or train you must use the OV-chipkaart (public transportation chip card). There are still ticket vending machines on bigger railroad stations that can produce a train ticket. You can also buy a ticket online. There is no alternative for the OV-chip card for buses.

What to do in Nijmegen

The website Visit Nijmegen provides lots of information about what to do in Nijmegen.