Related papers: Case Studies in Formal Reasoning About Lambda-Calc…
Higher-order representations of objects such as programs, proofs, formulas and types have become important to many symbolic computation tasks. Systems that support such representations usually depend on the implementation of an intensional…
In order to work with mathematical content in computer systems, it is necessary to represent it in formal languages. Ideally, these are supported by tools that verify the correctness of the content, allow computing with it, and produce…
We bring forward a logical system of transition algebras that enhances many-sorted first-order logic using features from dynamic logics. The sentences we consider include compositions, unions, and transitive closures of transition…
We study transformational program logics for correctness and incorrectness that we extend to explicitly handle both termination and nontermination. We show that the logics are abstract interpretations of the right image transformer for a…
Foundational verification considers the functional correctness of programming languages with formalized semantics and uses proof assistants (e.g., Coq, Isabelle) to certify proofs. The need for verifying complex programs compels it to…
Autoformalization has emerged as a term referring to the automation of formalization - specifically, the formalization of mathematics using interactive theorem provers (proof assistants). Its rapid development has been driven by progress in…
We propose a $\lambda$-calculus-style formal language, called the $\mu$-syntax, as a lightweight representation of the structure of cyclic operads. We illustrate the rewriting methods behind the formalism by giving a complete step-by-step…
Large Language Models (LLMs) have demonstrated impressive capabilities in structured reasoning and symbolic tasks, with coding emerging as a particularly successful application. This progress has naturally motivated efforts to extend these…
The linear-algebraic lambda-calculus and the algebraic lambda-calculus are untyped lambda-calculi extended with arbitrary linear combinations of terms. The former presents the axioms of linear algebra in the form of a rewrite system, while…
This paper presents a logical approach to the translation of functional calculi into concurrent process calculi. The starting point is a type system for the {\pi}-calculus closely related to linear logic. Decompositions of intuitionistic…
The termination method of weakly monotonic algebras, which has been defined for higher-order rewriting in the HRS formalism, offers a lot of power, but has seen little use in recent years. We adapt and extend this method to the alternative…
Classical Processes (CP) is a calculus where the proof theory of classical linear logic types communicating processes with mobile channels, a la pi-calculus. Its construction builds on a recent propositions as types correspondence between…
The lambda calculus with constructors is an extension of the lambda calculus with variadic constructors. It decomposes the pattern-matching a la ML into a case analysis on constants and a commutation rule between case and application…
A natural next step in the evolution of constraint-based grammar formalisms from rewriting formalisms is to abstract fully away from the details of the grammar mechanism---to express syntactic theories purely in terms of the properties of…
Formalised libraries of combinatorial mathematics have rapidly expanded over the last five years, but few use one of the most important tools: probability. How can often intuitive probabilistic arguments on the existence of combinatorial…
We describe a Martin-L\"of-style dependent type theory, called Cocon, that allows us to mix the intensional function space that is used to represent higher-order abstract syntax (HOAS) trees with the extensional function space that…
We present an approach for representing abstract argumentation frameworks based on an encoding into classical higher-order logic. This provides a uniform framework for computer-assisted assessment of abstract argumentation frameworks using…
We advocate the use of de Bruijn's universal abstraction $\lambda^\infty$ for the quantification of schematic variables in the predicative setting and we present a typed $\lambda$-calculus featuring the quantifier $\lambda^\infty$…
The $\lambda$-superposition calculus is a successful approach to proving higher-order formulas. However, some parts of the calculus are extremely explosive, notably due to the higher-order unifier enumeration and the functional…
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.…