Mathematical Structures in Formal System Development and Analysis

invited speakers

• Daniel Găină Institute of Mathematics for Industry, Kyushu University Japan biography Daniel Găină is an assistant professor at the Institute of Mathematics for Industry at Kyushu University, Japan. He received his PhD degree from the Japan Advanced Institute of Science and Technology (JAIST) in 2009, and continued his career at JAIST until 2017. During that time, he worked on the algebraic specification language CafeOBJ, providing support for Observational Transition Systems and enhancing its modularity. He joined the Institute of Mathematics for Industry in the spring of 2017. His current research focuses on the use of advanced model theory and category theory in order to develop solid mathematical foundations for the reconfiguration paradigm, which includes the design and implementation of a verification method for transition systems.

• Andrei Pavelescu University of South Alabama USA biography Andrei Pavelescu is an assistant professor in the Mathematics Department at University of South Alabama. He received his Ph.D. degree from USC in 2012 under the supervision of Dr. Robert Guralnick. His main research focus lies within the realm of (finite) group theory and graph theory, although he also had encounters with number theory, ring theory and orderable groups.

• Andrei Popescu Middlesex University London United Kingdom biography Andrei holds Ph.D. degrees in computer science from the University of Illinois at Urbana-Champaign and in mathematics from the University of Bucharest. Between 2010 and 2014 he worked as a postdoc at the Technical University of Munich. From 2014, he has been a Senior Lecturer at Middlesex University London. His research interests include theorem proving, (co)inductive datatypes, syntax with bindings, logical foundations, proof-assistant automation and verification of information-flow security. One of his main research vehicles is the Isabelle proof assistant. Together with colleagues, he has been developing Isabelle/HOL's infrastructure for (co)inductive datatypes and the verified conference management system CoCon. In the past, he worked on abstract model theory and fuzzy logic.

• Ferucio Laurențiu Țiplea Alexandru Ioan Cuza University of Iași Romania biography Ferucio Laurențiu Țiplea is a professor at the Alexandru Ioan Cuza University of Iași, Romania. He received his MSc and PhD degrees from the Alexandru Ioan Cuza University of Iași in 1986 and 1993, respectively. From 1990 to 1991 he was a member of the Faculty of Mathematics of the Alexandru Ioan Cuza University. He joined the Faculty of Computer Science in the autumn of 1991. His research interests include the high-level modelling, design and analysis of systems; cryptography and computer security; and algebraic foundations of computer science.

• Uwe Egbert Wolter University of Bergen Norway biography Uwe E. Wolter is associate professor at the University of Bergen, Norway. He received his PhD degree in 1989 from the Technical University Magdeburg, Germany. He was awarded with the Medal of Honour from the East-German Society of Mathematics for the best PhD thesis of the year. He held positions at Humboldt-University Berlin and Technical University Berlin before joining the Department of Informatics at the University of Bergen in 2000. His research interests can be characterized in two ways: Foundation of Formal Specifications, the broad topic, and Applied Category Theory, the method. He contributed to areas like Algebraic Specification, Abstract Model Theory, Graph Transformation, Coalgebra, Process Calculi and Knowledge Engineering. The last decade his research focuses on the foundation of model-driven software engineering.

programme

tuesday, 2^nd July

11:15–11:30

Registration & Opening

11:30–12:20

Andrei Popescu

The definitional approach in proof assistants based on higher-order logic

Higher-Order Logic (HOL) is the foundation of some major proof assistants in current use. A crucial characteristic of developments in HOL-based proof assistants is the definitional approach: Whenever possible, concepts are introduced by definitions rather than arbitrary axioms. I will discuss the significance of following the definitional approach for the logical trustworthiness of formal developments. Then I will describe mathematical formulations of trustworthiness, having different degrees of strength – safety, conservativity and consistency – and I will compare and contrast model-theoretic and proof-theoretic techniques to prove them.

General congress activities & Lunch break

15:00–15:50

Uwe Egbert Wolter

Indexed vs. fibred structures in specification formalisms – A field report

Based on experiences in areas like Algebraic Specifications, Institutions, Graph Transformations, Coalgebras and Foundations of Model Driven Software Engineering, I will discuss the use of indexed and fibred structures in specification formalisms – their relationship as well as their advantages and disadvantages. Especially, I will address the topics model amalgamation, Grothendieck construction, van-Kampen square and (deep) meta-modeling. As a sample specification formalism, I will outline the Diagram Predicate Framework, a variant of the "generalized sketch" framework.

Tea/coffee break

16:30–17:20

Ferucio Laurențiu Țiplea

Quadratic residuosity based cryptography
(joint with the Number Theory special session)

The quadratic residuosity problem is the problem to distinguish between the distributions of quadratic residues and quadratic non-residues modulo a composite integer. The intractability of the quadratic residuosity problem is the basis for the security of numerous constructions in cryptography, such as public-key and identity-based encryption schemes, pseudo-random generators, or cryptographic protocols. The aim of this talk is to provide a general overview on quadratic residuority problem and its applications to cryptography. Aspects related to the gap group of signed quadratic residues will also be discussed.

17:30–17:55

Adriana Balan

Distributivity over finite residuated lattices

The familiar adjunction between ordered sets and completely distributive lattices can be extended to generalised metric spaces, that is, categories enriched over a quantale. The crucial point is an appropriate distributive law between the "down-set" monad and the "up-set" monad on the category of quantale-enriched categories. If the base quantale is a finite MTL-algebra, this distributive law can be concretely formulated in terms of operations, equations and choice functions, similar to the familiar distributive law of lattices.

18:00–18:25

Claudia Chiriță

The hitchhiker's guide to Haskell: understanding type-class polymorphism 

We present two important features of the Haskell programming language, polymorphism and type-class polymorphism, to the dwellers of the model-theory universe. We start from higher-order logic with Henkin semantics (HNK), which allows us to capture some basic Haskell concepts and programs. Then, building on ideas from existing work on dealing with type-class polymorphism in an institutional setting, we outline a way of extending HNK to allow for parametric data types and polymorphic functions.

18:30–19:20

Daniel Găină

Forcing and calculi for hybrid logics

The concept of institution formalizes the intuitive notion of logic in a category-based setting. Similarly, the definition of hybrid institution captures the concept of hybrid logic, i.e. a type of modal logic expressive enough to allow references to the states of the models. In formal methods, hybrid logics are recognized as being suitable for describing reconfigurable systems. The present contribution sets the foundation of a formal verification methodology for reconfigurable systems by defining a proof calculus in an arbitrary hybrid institution. In order to prove completeness, the paper introduces the forcing technique for hybrid institutions and studies a forcing property based on syntactic consistency. The proof calculus is shown to be complete and the general results are instantiated to several benchmark examples of hybrid logical systems.

wednesday, 3^nd July

9:00–9:25

Ionuț Țuțu

Kripke congruences

In universal algebra, the notion of congruence captures precisely those equivalence relations that allow for a natural algebraic structure to be defined on equivalence classes. This provides an important basic tool for building initial models and for proving completeness results in equational logics. In this talk, we take a category-theoretic route to defining congruences on Kripke structures by exploring a connection with universal constructions such as that of kernel pair and quotient object. The end result is a universal property of Kripke quotients, which we then use to show that every set of equational statements (in a suitable hybrid logic) admits an initial Kripke model.

9:30–10:20

Andrei Pavelescu

Intrinsic linking in (self complementary) graphs

A simple graph is called intrinsically linked if every embedding of it into $R^3$ contains a non-trivial link. Campbell et al. showed that a graph on $n \geq 6$ vertices and at least $4n − 9$ edges is intrinsically linked because it contains a $K_6$; this implies that for a graph $G$ with $n \geq 15$ vertices, either $G$ or its complement is intrinsically linked. We improve this result by proving that given any simple non-oriented graph $G$ with at least thirteen vertices either $G$ or its complement is intrinsically linked. In the process, we discuss the de Verdière invariant, an algebraic construction which yields surprising results about the topological properties of a graph. We also discuss some constructions which attain maximal Hadwiger number for self complementary graphs.

10:30–10:55

Mihai Codescu

H – A tool for formal specification and verification of reconfigurable systems 

We present a tool for the specification and verification of reconfigurable systems. These are systems that have different modes of operation and commute between those modes during their execution as response to events. The foundation of the tool is provided by a generic method of adding features characteristic to hybrid logic, both at the syntactic and the semantic level, over an arbitrary base institution, via a process called hybridisation. Automated proof support for the logic thus obtained is provided via a generic methodology of proof-by-translation, where a conjecture is first translated to first-order logic then verified there using automated first-order provers. We describe how the hybridisation method and a language for specification of reconfigurable systems are implemented in an extension of the Heterogeneous Tool Set.

Tea/coffee break

11:30–13:00

Type theory or Model theory?

Andrei Popescu interviewed by Răzvan Diaconescu

General guidelines for the audience

1. The interview will consist of a dialogue between Andrei Popescu and Răzvan Diaconescu.
2. This means that there will be absolutely no verbal interaction with the audience.
3. However, the members of the audience are welcome to submit questions or comments for the interviewer to consider and introduce into the dialogue at the most appropriate moment.
4. All questions or comments should be submitted in written form either by e-mail to Răzvan Diaconescu before the interview (which is highly encouraged), or on a small piece of paper during the event.
5. These rules will be *observed strictly*. For those who find them inconvenient, in order to avoid a personal discomfort, it would be worth considering not to participate.

Conclusions & Lunch break

contact

If you have any questions or inquiries, you can contact the organizers via e-mail:

• Răzvan Diaconescu
• Ionuț Țuțu