Related papers: Proofs and Programs about Open Terms
Program logics are a powerful formal method in the context of program verification. Can we develop a counterpart of program logics in the context of language verification? This paper proposes language logics, which allow for statements of…
Structural proof theory is praised for being a symbolic approach to reasoning and proofs, in which one can define schemas for reasoning steps and manipulate proofs as a mathematical structure. For this to be possible, proof systems must be…
We consider the problem of automated reasoning about dynamically manipulated data structures. The state-of-the-art methods are limited to the unfold-and-match (U+M) paradigm, where predicates are transformed via (un)folding operations…
Declarative styles such as functional programming (FP) are rapidly gaining ground on their imperative cousins, including procedural and object-oriented programming. The shift is subtle because it is happening within the context of…
LLM-generated explanations can make technical content more accessible, but there is a ceiling on what they can support interactively. Because LLM outputs are static text, they cannot be executed or stepped through. We argue that grounding…
Design patterns are distilled from many real systems to catalog common programming practice. However, some object-oriented design patterns are distorted or overly complicated because of the lack of supporting programming language constructs…
For those of us who generally live in the world of syntax, semantic proof techniques such as reducibility, realizability or logical relations seem somewhat magical despite -- or perhaps due to -- their seemingly unreasonable effectiveness.…
This book can be seen either as a text on theorem proving that uses techniques from general algebra, or else as a text on general algebra illustrated and made concrete by practical exercises in theorem proving. The book considers several…
Deep neural networks successfully pervaded many applications domains and are increasingly used in critical decision processes. Understanding their workings is desirable or even required to further foster their potential as well as to access…
This paper develops an algorithmic-based approach for proving inductive properties of propositional sequent systems such as admissibility, invertibility, cut-elimination, and identity expansion. Although undecidable in general, these…
We examine the practicality for a user of using Answer Set Programming (ASP) for representing logical formalisms. We choose as an example a formalism aiming at capturing causal explanations from causal information. We provide an…
User defined recursive types are a fundamental feature of modern functional programming languages like Haskell, Clean, and the ML family of languages. Properties of programs defined by recursion on the structure of recursive types are…
In this paper we introduce a Conditional Answer Set Programming framework (Conditional ASP) for the definition of conditional extensions of Answer Set Programming (ASP). The approach builds on a conditional logic with typicality, and on the…
The safety of automated driving systems must be justified by convincing arguments and supported by compelling evidence to persuade certification agencies, regulatory entities, and the general public to allow the systems on public roads.…
Program equivalence in linear contexts, where programs are used or executed exactly once, is an important issue in programming languages. However, existing techniques like those based on bisimulations and logical relations only target at…
We investigate the formal semantics of a simple imperative language that has both classical and quantum constructs. More specifically, we provide an operational semantics, a denotational semantics and two Hoare-style proof systems: an…
We present Dependent Lambek Calculus, a domain-specific dependent type theory for verified parsing and formal grammar theory. In $\textrm{Lambek}^D$, linear types are used as a syntax for formal grammars,and parsers can be written as linear…
This thesis embarks on a comprehensive exploration of formal computational models that underlie typed programming languages. We focus on programming calculi, both functional (sequential) and concurrent, as they provide a compelling rigorous…
Causal models are playing an increasingly important role in machine learning, particularly in the realm of explainable AI. We introduce a conceptualisation for generating argumentation frameworks (AFs) from causal models for the purpose of…
We present three projects concerned with applications of proof assistants in the area of programming language theory and mathematics. The first project is about a certified compilation technique for a domain-specific programming language…