Embedded Files
09-07-2024
09-07-2024
All the times are CEST+1 (Tallinn time)
Registration 8:00 - 8:55
8:55 - 9:00
Kickoff
Kickoff
9:15 - 9:30
9:30 - 9:45
On the Satisfiability of Context-free String Constraints with Subword-Ordering and Transduction
C Aiswarya, Soumodev Mal and Prakash SaivasanAbstract
Break 10:00 - 10:30
10:30 - 10:45
A Uniform Framework for Language Inclusion Problems
Chana Weil-Kennedy, Kyveli Doveri and Pierre GantyAbstract
10:45 - 11:00
Combining Quantum and Classical Control
Kinnari Dave, Louis Lemonnier, Romain Pechoux and Vladimir ZamdzhievAbstract
11:00 - 11:15
Classification Transfer for CSPs via Algebraic Products
Manuel Bodirsky, Peter Jonsson, Barnaby Martin, Antoine Mottet and Žaneta SemanišinováAbstract
11:15 - 11:30
Interpretations of the logic of FDE in terms of information and evidence
Ana Clara Rezende and Abílio RodriguesAbstract
11:45 - 12:30
Invited Talk: Constructive Interactions
Sandra KieferInvited Talk: Constructive Interactions
The broader topic of this talk are interactions in computer science research.The first part of the talk will deal with pairwise interactions between agents as a means for formal modelling of exchange of information to model distributed computing. I will give a very brief and light introduction to population protocols and to the situation when the agents in such a protocol carry data and observe each other. I will present a teaser overview of the techniques that we use to study verification problems on these protocols.The corresponding project was started between researchers of different backgrounds in computer science at a workshop. The second part of the talk considers constructive interactions on an intradiegetic level, that is, at the level of the authors instead of the protagonists of work in logic in computer science. I will elaborate on the value of networks and communities in our field and share some of my thoughts on dynamics between researchers as well as suggestions for fruitful collaborative approaches.
Lunch 12:30 - 14:00
14:00 - 14:45
Invited Talk: Types for (Slow) AI
Viviana BonoInvited Talk: Types for (Slow) AI
Reasoning on knowledge bases is often done by machine learning models fed with W3C Resource Description Framework data rather than by applying formal inference techniques. On the one hand, this use of machine learning certainly provides a faster mechanism than any formal (run time) inference technique, but, on the other hand, it may lead to an impoverishment of the expressivity of the properties proven. Statically typed languages can help to attenuate the performance issue: they offer the possibility of checking or inferring certain properties of interest statically, meaning that they do not slow down run time. In this talk, we will survey some already-present applications of types to knowledge representation and give a hint about open problems.
Chair: Luigi Liquori
14:45 - 15:00
15:00 - 15:15
Break 15:30 - 16:00
16:00 - 16:45
Invited Talk: New Techniques for Sound Language Interoperability
Designers of typed programming languages commonly prove meta-theoretic properties such as type soundness and, if applicable, security properties such as noninterference, for at least a core of their language. But any practical language implementation must provide some way of interoperating with code written in other languages -- usually via a foreign-function interface (FFI) -- which opens the door to new, potentially unsafe and insecure, behaviors that aren't accounted for in the original type soundness or security proofs. Despite the prevalence of interoperability in practical software, principled foundations for the end-to-end design, implementation, and verification of interoperability mechanisms have been largely neglected. In this talk, I'll present two different approaches for ensuring sound interoperability between practical languages where interoperation is implemented using glue code that mediates interaction between languages after compilation to a common lower-level intermediate representation (IR). The first approach is a technique verifying soundness of the FFI and involves building a _semantic intermediate representation_: a semantic model of source-language types as relations on terms of the lower-level IR. Semantic IRs can be used to guide the design and implementation of sound FFIs and to verify that the IR glue code used to implement conversions ensures type soundness. The second approach involves use of type-preserving compilation down to a richly typed intermediate language where link-time type checking can catch any type soundness violations that arise from interoperation. Specifically, we've designed RichWasm, a richly typed IR that sits atop WebAssembly but relies on capability types to ensure safe fine-grained shared-memory interoperability between Wasm modules compiled from a GC'd language and a language with manually managed memory.Invited Talk: New Techniques for Sound Language Interoperability
16:45 - 17:45
Round Table: Women in industry and academia
Kait O'Neil, Greta Yorsh, Amal Ahmed, Aiswarya. C. (i.s.)Cocktail party 19:00 - 21:00
Page updated
Google Sites
Report abuse