ABSTRACT. In syntactic anti-unification, one is concerned with finding the commonalities between terms, while (uniformly) abstracting their differences. The original goal of anti-unification development in the seventies was to automate inductive reasoning. Recent applications of anti-unification techniques include efficiently transforming sequential code into parallel code, detecting code clones, and preventing software failures. Previous work addressed the elements required to verify, in the Prototype Verification System (PVS), termination and soundness of a functional algorithm based on inference rules for syntactic anti-unification. This paper dissects all aspects required to formally establish the completeness of the rule-based algorithm, highlighting the significant differences in the formalizations of anti-unification and unification.

ABSTRACT. The challenges of formalization of lambda-calculi in proof assistants do not come only from the adequate representation of binding. Different kind of challenges come from substitution operations which are not based on the conventional replacement of a free occurrence of a variable by a term that lives in the same syntactic class of the variable. Example of such unconventional substitution operations are abundant. In this work we consider four systems with unconventional substitution, two of which are isomorphic to the ordinary lambda-calculus, as a case study in support provided by a mainstream assistant endowed with a library mechanizing a mainstream binding representation. Specifically, we develop a formalization of some basic metatheory in Rocq helped with the Autosubst library. The development profits from the support about binding, but the boilerplate relative to the unconventional substitutions benefits of no automation.

ABSTRACT. Autosubst enables automatic equality-checking up to the sigma-calculus for assumption-free equalities, allowing users to avoid cumbersome reasoning about de Bruijn indices. While effective in many cases, this approach is inapplicable when matching against typing rules, reduction relations, or lemmas, requiring users to either phrase typing rules in a way that they work with Autosubst or even stating explicitly an alternative de Bruijn term. But even without beta-reduction, solutions of matching may be non-unique. This paper presents a work-in-progress method for automatically pattern matching against assumptions, evaluated on standard case studies including the POPLMark and POPLMark Reloaded challenges.

ABSTRACT. We formalize strong barbed similarity for the $\pi$-calculus in the Beluga proof assistant, completing a line of work addressing the Concurrent Calculi Formalization Benchmark. By extending previous developments to include replication, we give a coinductive encoding of behavioral equivalence based on barbs and internal actions. Using Beluga’s copattern-based coinduction, we obtain concise and compositional proofs, including compatibility properties and a context lemma characterizing barbed precongruence. The case study demonstrates the effectiveness of combining HOAS and coinductive reasoning for mechanizing concurrent calculi.

ABSTRACT. This paper introduces the strategy language of Pgeon, a meta-prover with a clear separation between inference rules and proof search. We give the semantics of strategies as functions over proof states, and of the operators that are used to combine them, allowing for sequential composition, choice, repetition and interleaving of strategies. This language is designed to handle the challenge of fair proof search in semi-decidable logics, where simple depth-first exploration of the proof space is not guaranteed to achieve completeness. We showcase the expressiveness and effectiveness of the approach through case studies in first-order and modal logics.

ABSTRACT. Miller and Tiu’s generic quantification (i.e., the ∇ quantifier) brings a logical treatment of the common concepts of name and freshness. Unlike the related fresh quantifier of nominal logic, generic quantification has been defined proof theoretically. In fact, several generic quantifiers have been considered. In the earlier version, nabla is defined as a self-dual quantifier commuting with all propositional connectives. Later, it has been extended to satisfy two additional properties: ∇x.∇y.F is equivalent to ∇y.∇x.F; ∇x.F is equivalent to F if x does not occur in F. Together, the two properties imply nominal logic’s equivariance principle. While they have not been considered independently so far, it is natural to consider the two properties individually, giving rise to four quantifiers. Taking inspiration from substructural proof theory, we call the first property exchange and the second one weak- ening, and define uniformly four logics through proof systems with substructural generic contexts. We then consider the problem of giving a (sound and complete) truth seman- tics for these logics. We build upon earlier work by Goubault-Larrecq, which proposed a complete semantics for Miller and Tiu’s early nabla quantifier, and show that (enriched) nabla sets can be used to define, in a uniform way, a semantics for the four substructural generic logics. We show that this semantics is sound and complete for three of the logics, defined through their natural (classical) sequent calculi. However, we identify a mismatch for the case where nabla satisfies weakening but not exchange: in that case, the natural proof system is not sound for our semantics.

ABSTRACT. This paper examines the foundational distinctions between proof theory and dependent type theory (DTT) in the design of interactive theorem provers. While several implemented systems are designed using the dependently typed lambda-calculus to represent proofs, no major proof assistant is designed using modern structural proof theory, even though, as I will argue here, the sequent calculus offers a compelling alternative framework. Six specific topics are proposed where the proof-theoretic perspective is arguably superior to the DTT perspective. These topics include the separation of logic from proof structure, the strategic use of non-determinism in proof reconstruction, and the avoidance of complex typing-discipline issues such as universe levels and proof irrelevance. The final topic---the treatment of bindings---is further developed to demonstrate how a natural, intensional approach is achieved through the mobility of binders. This methodology is illustrated via the Abella theorem prover, which leverages lambda-tree syntax and the nabla-quantifier to provide an elegant environment for reasoning about the meta-theory of languages and logics involving complex binding.