Keynotes

Marie Duží

Title: Hyperintensions as Structured Procedures

Transparent Intensional Logic (TIL) is a higher-order, hyperintensional, typed -calculus with a procedural semantics. The terms of the ideography of TIL denote procedures producing mappings rather than the mappings themselves. Mappings are semantically secondary, while the procedures are semantically primary. Procedures are sui generis objects of the ontology of TIL. I first introduce six kinds of TIL procedures. There are two kinds of atomic procedures that supply objects to operate on by molecular procedures, namely Trivialization and variables, and two basic kinds of molecular procedures, (-)Closure and Composition. Closure is the procedure of producing a functional mapping by abstracting over the values of -bound variables. Composition is the procedure of applying a function to its arguments. There is a pair of dual procedures operating on lower-order procedures, namely Trivialisation (0C) and Double Execution (2C). While 0C displays the procedure C as an object to operate on, 2C cancels the displaying effect, as 2C produces what is produced (if anything) by the procedure produced by C. It means that while in 0C the procedure C occurs hyperintensionally rather than in the execution mode, in 2C it occurs extensionally.
Having introduced TIL fundamentals, I address and solve a technical problem arising in the hyperintensional procedural semantics of this system. The problem concerns variable binding. A pair of procedures that are duals of one another work together well in the standard cases. But there are limiting cases where they fail to. One of the procedures, Trivialization, when applied to another procedure, raises the logical type of this procedure and makes it technically feasible to operate on this procedure itself rather than the product it is typed and structured to yield. Any occurrences of variables within the procedure become Trivialization-bound. The other procedure, Double Execution, when applied to another procedure, is typed and structured to, first, obtain the product of this procedure and, second, obtain the product of this product on condition that the latter is itself a procedure. Double Execution lowers the logical type of the procedure it is applied to. It is a feature of Double Execution that its execution produces entities beyond the second procedure. As a result, there are cases where Trivialization-bound occurrences of variables become free occurrences; new variables that are apparently free for substitution can emerge by executing Double Execution. This is something we do not want to happen. These cases undermine our definition of substitution, which in turn jeopardizes the validity of the rules of -conversion, not least -conversion. The technical result I present is a principled, as opposed to ad hoc, definition of substitution, which introduces the restrictions required. I also argue that it is not an option to solve the problem by jettisoning one of the two procedures, as both are indispensable and, thus, must be made to work properly together as duals. The problem I address and solve extends beyond Transparent Intensional Logic. Any logic or programming language with a high degree of expressive power is liable to confront a comparable problem with variable binding.

Bio:

Born 1948 in Ostrava, Czech Republic. In 1971, she graduated in mathematics from Masaryk University of Brno, and in 1982, obtained here the degree RNDr. Until the velvet revolution, she worked as a programmer and analyst in various software companies in then Czechoslovakia. After the revolution, she became an assistant professor in Charles University of Prague, teaching logic and foundations of computer science. Since 2001 till now, in VSB-Technical University of Ostrava, where she habilitated and finally in 2016 obtained the degree of professor of computer science. Published more than hundred papers indexed in WoS and Scopus and two books (with co-authors Bjorn Jespersen and Pavel Materna), mostly dealing with Transparent Intensional Logic (TIL).

Linh Anh Nguyen

Title: Bisimulations between Fuzzy Structures
Bisimulation is a concept in computer science and mathematical logic used to define the notion of equivalence between systems. It has been widely studied for various kinds of graph-based structures, such as Kripke models, labeled transition systems, automata, social networks and interpretations in description logics. It can be exploited for minimizing a system and for the classification and clustering problems. To deal with vagueness and impreciseness, fuzzy graph-based structures are used instead of crisp ones. There are two kinds of bisimulation, crisp and fuzzy, between fuzzy graph-based structures. While crisp bisimulations characterize indiscernibility of states, actors or individuals, fuzzy bisimulations characterize similarity between them. The talk presents an overview of results on logical characterizations and computation of bisimulations between uzzy structures.
Bio: Linh Anh Nguyen received the M.Sc., Ph.D., and Habilitation degrees in computer science from the University of Warsaw, Poland, in 1997, 2000, and 2009, respectively. He is currently an Associate Professor with the Institute of Informatics, University of Warsaw, Poland, and the Faculty of Information Technology, Nguyen Tat Thanh University, Vietnam. His current research interests include simulations and bisimulations for fuzzy systems, automated reasoning and rule-based languages in modal/description logics.

Prof Maria Papadopouli

Title: Identifying Neuronal Modules of Communication in Primary Visual Cortex

Bio:

Maria Papadopouli (Ph.D. Columbia University, October 2002) is a Professor of Computer Science at the University of Crete, a Research Associate at the Institute of Computer Science, FORTH, and a Fulbright Scholar. She has been a visiting Professor at  the Brigham and Women’s Hospital, Harvard Medical School (2022-2023), the Computer Science and Artificial Intelligence Laboratory (CSAIL), MIT (2017), and at the School of Electrical Engineering, KTH Royal Institute of Technology in Stockholm. From July 2002 until 2006, she was a tenure-track Assistant Professor at the University of North Carolina at Chapel Hill (UNC) (on leave from July 2004 until June 2006. Her research has been supported by several awards (e.g., IBM Faculty Awards, Google Faculty Award, Comcast Innovation Fund. and competitive national, EU, and international grants. She has been selected in the N2Women Stars in Networking and Communications in 2021.