Seminars

Thursday, May 23, 2024: Sergey Goncharov (FAU of Erlangen and Nürnberg)

Time: 10:15 - 11:00
Location: BA 406 (Bajuwarenstrasse 4, 4th floor) and https://uni-regensburg.zoom-x.de/j/9999678980
 

Title: Higher-Order Program Equivalence in the Abstract

Abstract: Reasoning about program equivalence in higher-order setting is one of the central topics in computer science, with the classical lambda-calculus as a prototypical example and with its countless flavors and extensions thereof, all the way up to Haskell and OCaml. A recently emerged program of higher-order mathematical operational semantics aims to abstract and unify reasoning methods for such languages on the basis of two parameters: the language syntax and its (small-step) operational semantics. I will present our latest results within this ongoing effort, namely, a general construction of (step-indexed) logical relations, as an abstract sound method for proving contextual equivalence of programs, i.e. their equivalent behavior under any program context.

Wednesday, March 27, 2024: Simon Guilloud (EPFL)

Time: 10:15 - 11:00
Location: BA 607 (Bajuwarenstrasse 4, 6th floor) and https://uni-regensburg.zoom-x.de/j/9999678980
 

Title: Using Orthologic in Automated Reasoning

Abstract: Orthologic is a logical system whose underlying algebra is that of ortholattices (relaxations of boolean algebras which don't necessarily satisfy the distributive law). Because validity of formulas in orthologic can be decided in polynomial time, we are interested in their applicability to efficient and predictable automated reasoning. This talk will present a collection of algorithmic and logical results about orthologic, and explain how it was implemented in the program verifier Stainless and the proof assistant Lisa.

Thursday, November 30, 2023: Julie Cailler (University of Regensburg)

Time: 10:15 - 11:00
Location: BA 607 (Bajuwarenstrasse 4, 6th floor) and https://uni-regensburg.zoom-x.de/j/64045918898
 

Title: Designing an Automated Concurrent Tableau-Based Theorem Prover for First-Order Logic

Abstract: Automated Theorem Proving (ATP) involves the use of formal methods to automatically (dis)prove logical formulas. Its primary applications include bug detection in critical systems and assistance in demonstrating mathematical proofs.

This talk focuses on the presentation of Goéland, a concurrent automated theorem prover, and the main challenges it encounters. These challenges include implementing a fair tableau-based proof-search procedure, addressing theory reasoning, and ensuring the generation of machine-checkable proofs.

Thursday, November 16, 2023: Franziska Alber (University of Regensburg)

Time: 10:15 - 11:00
Location: BA 607 (Bajuwarenstrasse 4, 6th floor) and https://uni-regensburg.zoom-x.de/j/62895178597
 

Title: Complementation of Parametric Finite State Automata

Abstract: Finite State Automata (FSAs) are a well-researched model of computation where each FSA corresponds to a regular language. In particular, determinisation and complementation are well-understood: while a FSA may be nondeterministic, it is always possible to construct an equivalent deterministic FSA and use this construction to find a FSA that corresponds to the complement language.

Parametric Automata (PAs) are a generalization of finite state automata that are suited for handling infinite alphabets (and therefore, a wider array of formal languages). Transitions do not simply compare fixed letters, but may contain logical formulae or compare the input to nondeterministically assigned parameters. This increased power comes at a price: there is no definite, canonical way to define determinism for PAs, and unlike FSAs, PAs are not closed
under complementation (i.e., a complement may not exist!). We will explore different kinds of determinism for PAs and define several classes of PAs that can effectively be complemented.