The date for the annual meeting of the IFIP WG 1.6 is Wednesday, July 5, 2023. The meeting is co-located with FSCD 2023 and CADE 2023, and will take place during the third day of FSCD.
Abstract: In this talk, I will present Lambdapi, a proof assistant on top of the Dedukti logical framework, which extends Edinburg's Logical Framework LF or, equivalently, Martin-Löf's logical framework, but allowing objects and types to be defined by higher-order rewriting rules, possibly modulo commutativity, or associativity and commutativity together. Dedukti is a logical framework, that is, it does not come with a predefined logic. Instead one can define its own logic in it. This is used to encode not only the terms and propositions of many different provers but also the proofs that are actually developed in those provers. This goes from automated theorem provers based on first-order logic, interactive theorem provers based on Church's simple type theory like HOL-Light or Isabelle/HOL, to rich type systems like the ones of Coq, Agda or Lean. Rewriting is a key feature for encoding the proofs of those systems in Dedukti. Moreover, once a proof is encoded in Dedukti, it can be translated to other provers, depending on the deduction rules and features of the source system that are used in it, and the deduction rules and features of the target system. However, a number of properties of rewrite systems need to be checked by users for Lambdapi to behave properly like termination, confluence and preservation of typing, aka subject reduction. To this end, Lambdapi provides some useful tools: exports to the XTC and HRS formats, a procedure for checking subject-reduction automatically, and a procedure for checking local confluence incrementally.
Abstract: Quantitative extensions of equality characterize the approximation degree between objects. Fuzzy proximity and similarity relations are notable examples of such extensions. These and similar relations are used to model concepts such as vagueness, uncertainty, imprecision, imperfectness. Various approaches to formalizing quantitative information lead to the development of well-known logical, algebraic, and topological formalisms and structures such as e.g., fuzzy logic, rough logic, metric algebras, quantitative algebras, metric and proximity spaces, etc.
Symbolic constraint solving is ubiquitous in many areas of mathematics and computer science. Unification, matching, anti-unification, disunification, and ordering constraints are some prominent examples that play an important role in automated reasoning, term rewriting, declarative programming, and their applications. In this talk, we present recent advances in solving unification and anti-unification constraints in theories where equality is replaced by its quantitative approximation. Our algorithms solve unification, matching, and anti-unification problems modulo fuzzy tolerance (i.e., reflexive and symmetric but not necessarily transitive) relations where mismatches between symbol names and arities are permitted. We will discuss general principles behind these techniques, show examples, present some of the algorithms, and characterize their properties.
Abstract: Tree automata are a formalism based on term rewriting to represent unbounded regular sets of terms. The first attempts to use tree automata for program verification date back to 1987. Since then, a long standing research activity has tried to improve these first results to expand their applicability, improve their verification power, or explore their theoretical limits. During those 40 years of research, this small community came up with many results but very few applications to real verification problems. Verification of cryptographic protocols being one of them. However, several recent papers from the formal verification community suggest that new applications may arise. A first application is the automatic verification of real size higher-order functional programs. Another application is the extension of SMT solvers with regular tree languages techniques to automatize the verification of programs manipulating Algebraic Data Types.
10:30 - 12:30: Session 1
- 50' Thomas Genet: Using Tree Automata for Verification, at last
- 20' the International School on Rewriting by Aart Middeldorp
- 50' Temur Kutsia: Symbolic techniques for quantitative extensions of equality
12:30 - 14:00: Break
14:00 - 15:45: Session 2
- 50' Frédéric Blanqui: Lambdapi, a proof assistant using rewriting
- 25' the Rewriting Website by Luigi Liquori
- 30' business meeting (members-only)
The meetings of the working group are public, with the single exception of the business meeting.