Archivo de seminarios
Flexible and Expressive Typed Path Patterns for GQL
27 de mayo de 2026
Abstract:
Graph databases have become an important data management technology across various domains, including biology, sociology, industry (e.g. fraud detection, supply chain management, financial services), and investigative journalism, due to their ability to efficiently store and query large-scale knowledge graphs and networks. Recently, the Graph Query Language (GQL) was introduced as a new ISO standard providing a unified framework for querying graphs. However, this initial specification lacks a formal type system for query validation. As a result, queries can fail at runtime due to type inconsistencies or produce empty results without prior warning. Solving this issue could have great benefits for users in writing correct queries, especially when handling large datasets. To address this gap, we introduce a formal type model for a core fragment of GQL extended with property-based filtering and imprecise types both in the schema and the queries. This model, named FPPC, enables static detection of semantically incorrect and stuck queries, improving user feedback. We establish key theoretical properties, including emptiness (detecting empty queries due to type mismatches) and type safety (guaranteeing that well-typed queries do not fail at runtime). Additionally, we prove a gradual guarantee, ensuring that removing type annotations either does not introduce static type errors or only increases the result set. By integrating imprecision into GQL, FPPC offers a flexible solution for handling schema evolution and incomplete type information. This work contributes to making GQL more robust, improving both its usability and its formal foundation.Basis-Sensitive Quantum Typing via Realisability
1 de julio de 2026
Abstract:
We present λB , a quantum-control λ-calculus that refines previous basis-sensitive systems by allowing abstractions to be expressed with respect to arbitrary—possibly entangled—bases. Each abstraction and let construct is annotated with a basis, and a new basis-dependent substitution governs the decomposition of value distributions. These extensions preserve the expressive power of earlier calculi while enabling finer reasoning about programs under basis changes. A realisability semantics connects the reduction system with the type system, yielding a direct characterisation of unitary operators and ensuring safety by
construction. From this semantics we derive a validated family of typing rules, forming the foundation of a type-safe quantum programming language. We illustrate the expressive benefits of λB through examples such as Deutsch’s algorithm and quantum teleportation, where basis-aware typing captures classical determinism and deferred-measurement behaviour within a uniform framework.Foundational Constraint Solving for Expressive Refinement Typing
26 de agosto de 2026
Abstract:
SMT-based program verifiers face two fundamental limits: expressiveness, because specifications must stay within the boundaries of SMT decidability, and trust, because the solver is a large, unverified artifact whose soundness bugs silently compromise every tool built on it. We address both with Flex, a foundational Constrained Horn Clause (CHC) solver built in Lean that reduces the trusted base to the kernel alone. Flex targets the CHCs that arise from refinement typing, a typing discipline that extends types with logical predicates to specify and verify correctness properties.
First, I will introduce refinement types, using Flux — a refinement type checker for Rust — to show how refinement typing reduces the problem of verification to CHC solving. Then I will show how Flex encodes CHCs as Lean propositions with existentially bound predicates and implements CHC solvers as tactics (meta-programs) that compute kernel-checkable proofs. Finally, I will demonstrate how targeting Flex as a backend for Flux lets us prove functional-correctness properties of low-level Rust libraries that lie beyond SMT's reach.