Skip to ContentSkip to Navigation
Research Bernoulli Institute Fundamental Computing

Research

The Fundamental Computing group conducts cutting-edge research on the foundations of computing with a focus on the development of rigorous methods for ensuring correct and reliable software. This is a scientific and societal challenge, which we address using logic, concurrency theory, discrete mathematics, and category theory.

(Co)algebraic methods in logic and semantics (prof.dr. Helle Hvid Hansen)

Logic and semantics provide the foundations for the formal analysis of software systems. Due to the vast complexity of such systems, it is essential to have appropriate abstraction techniques and methods for compositional reasoning. To this end, in this theme, we study the fundamental relationships between logic, structure and program behaviours using the methods of modal logic, algebra and coalgebra. Modal logics are widely used as specification languages in formal verification due to their good balance between expressive power and computational complexity.  Algebra is a well-established theory of compositionality. Coalgebra is a branch of applied category theory that provides a unifying framework for reasoning about the behaviours of many different types of systems, including automata, transition systems and Markov decision processes. A main contribution in coalgebra has been to show that modal logics for specifying system behaviours can be developed at the abstract level of coalgebra. Much of our work falls in the rich area of coalgebraic modal logic.

Formal methods for concurrency and distribution (prof. dr. Jorge A. Pérez)

Message-passing programs are the backbone of most distributed software infrastructures today. This theme targets the rigorous specification and analysis of these communicating programs. We specialize in specification languages based on process calculi, formal languages that express the interaction of concurrent processes. For analysis, we focus on type systems, a well-established static analysis technique able to detect errors before programs are executed. In particular, we investigate behavioral type systems, which codify the protocols that interacting processes should implement. The combination of process calculi with behavioral types results in a compositional approach to verify safety and liveness properties for communicating programs. Our recent work investigates the logical foundations of behavioral type systems: how fundamental principles such as “propositions as types” can inform the principled verification of message-passing programs.

Non-classical logics and their proof theory (dr. Revantha Ramanayake)

While classical (boolean) logic is the logic of truth (and logic gates), non-classical logics model a much wider range of concepts: dynamic behaviour of software programs, proofs-as-programs, resource-awareness, fuzzy reasoning, multi-agent epistemic reasoning, language grammars, and more. Proof theory is the branch of Logic that studies a logic based on a formal (mathematical) notion of its proof system and its proofs. Our research centres on non-classical logics and their proof theory. We use proof systems to prove properties of the logics, e.g. computational properties like (un)decidability and complexity, drawing on ideas from theoretical computer science and discrete mathematics. This approach relies on refined proof systems with good mathematical properties, motivating our research into their development (structural proof theory). We are also interested in automated theorem provers and automated tools (software) for non-classical logics, and the computer-formalised proofs.

Mathematical logic (prof. dr. Gerard R. Renardel de Lavalette)

The focus is on the proof theory of equational logic and Horn logic, and on intuitionistic logic. Intuitionism was created by L.E.J. Brouwer; its logic, formalized by A. Heyting, reappeared as the foundation of type theory with applications in programming and theorem proving. Equational logic is the formalization of algebraic equational reasoning, used in tools like Mathematica. Horn logic is the logic of formulae of the form A1 ∧⋯∧ An→B; it is the basis of the logic programming language Prolog. We focus on fundamental properties like completeness (is a given proof system strong enough to prove all true statements?) and exactness (does a certain model correspond to the structure of a logic?).

Last modified:09 November 2021 1.41 p.m.