Abstract
We propose a new collection of benchmark problems in mechanizing the metatheory of programming languages, in order to compare and push the state of the art of proof assistants. In ...particular, we focus on proofs using logical relations (LRs) and propose establishing strong normalization of a simply typed calculus with a proof by Kripke-style LRs as a benchmark. We give a modern view of this well-understood problem by formulating our LR on well-typed terms. Using this case study, we share some of the lessons learned tackling this problem in different dependently typed proof environments. In particular, we consider the mechanization in Beluga, a proof environment that supports higher-order abstract syntax encodings and contrast it to the development and strategies used in general-purpose proof assistants such as Coq and Agda. The goal of this paper is to engage the community in discussions on what support in proof environments is needed to truly bring mechanized metatheory to the masses and engage said community in the crafting of future benchmarks.
The theory of call-by-value solvability Accattoli, Beniamino; Guerrieri, Giulio
Proceedings of ACM on programming languages,
08/2022, Volume:
6, Issue:
ICFP
Journal Article
Peer reviewed
Open access
The semantics of the untyped (call-by-name) lambda-calculus is a well developed field built around the concept of solvable terms, which are elegantly characterized in many different ways. In ...particular, unsolvable terms provide a consistent notion of meaningless term. The semantics of the untyped call-by-value lambda-calculus (CbV) is instead still in its infancy, because of some inherent difficulties but also because CbV solvable terms are less studied and understood than in call-by-name. On the one hand, we show that a carefully crafted presentation of CbV allows us to recover many of the properties that solvability has in call-by-name, in particular qualitative and quantitative characterizations via multi types. On the other hand, we stress that, in CbV, solvability plays a different role: identifying unsolvable terms as meaningless induces an inconsistent theory.
Sampling β-normal linear λ-terms Bodini, Olivier; Singh, Alexandros; Zeilberger, Noam
Pure mathematics and applications,
06/2022, Volume:
30, Issue:
1
Journal Article
Peer reviewed
Open access
Leveraging our recent work on the enumeration of
-redices in closed linear λ-terms, we present an algorithm for sampling
-normal closed linear λ-terms and their corresponding maps. Such terms ...correspond to proofs of tautologies in implicational linear logic and their generation is of interest in various domains, including the testing of linear logic theorem provers.
The (In)Efficiency of interaction Accattoli, Beniamino; Dal Lago, Ugo; Vanoni, Gabriele
Proceedings of ACM on programming languages,
01/2021, Volume:
5, Issue:
POPL
Journal Article
Peer reviewed
Open access
Evaluating higher-order functional programs through abstract machines inspired by the geometry of the interaction is known to induce
space
efficiencies, the price being
time
performances often poorer ...than those obtainable with traditional, environment-based, abstract machines. Although families of lambda-terms for which the former is exponentially less efficient than the latter do exist, it is currently unknown how
general
this phenomenon is, and how far the inefficiencies can go, in the worst case. We answer these questions formulating four different well-known abstract machines inside a common definitional framework, this way being able to give sharp results about the relative time efficiencies. We also prove that non-idempotent intersection type theories are able to precisely reflect the time performances of the interactive abstract machine, this way showing that its time-inefficiency ultimately descends from the presence of higher-order types.
The paper shows that the use of a composition of objects representing a data structure, in fact, means the creation of a kind of information channels on their basis, along which the computation ...process spreads. In the case of applying the applicative computational technology, the computation process is started by means of the operation of applying the function object to the argument object. Two ways are presented to generate function objects — to use either lambda expressions or combinators to represent them. The first method uses an abstraction meta-operator and associated variables, which leads to the use of substitution systems with the potential for side effects. In the second method, only constant combinator objects participate in the construction of the function, and their application to the argument triggers a conversion based on rewriting rules, which does not cause a side effect. A practical solution to the problem of synthesizing a compositional data structure can be mixed, when both lambda terms and combinators are involved in the computations, which reduces the length of expressions. As a result, a data structure appears, which is composed of compositions of argument objects, equipped with a generated set of supporting function objects.
Towards a homotopy domain theory Martínez-Rivillas, Daniel O.; de Queiroz, Ruy J. G. B.
Archive for mathematical logic,
05/2023, Volume:
62, Issue:
3-4
Journal Article
Peer reviewed
Open access
An appropriate framework is put forward for the construction of
λ
-models with
∞
-groupoid structure, which we call
homotopic
λ
-models
, through the use of an
∞
-category with cartesian closure and ...enough points. With this, we establish the start of a project of generalization of Domain Theory and
λ
-calculus, in the sense that the concept of proof (path) of equality of
λ
-terms is raised to
higher proof
(homotopy).
This paper introduces a functional term calculus, called pn, that captures the essence of the operational semantics of Intuitionistic Linear Logic Proof-Nets with a faithful degree of granularity, ...both statically and dynamically. On the static side, we identify an equivalence relation on pn-terms which is sound and complete with respect to the classical notion of structural equivalence for proof-nets. On the dynamic side, we show that every single (exponential) step in the term calculus translates to a different single (exponential) step in the graphical formalism, thus capturing the original Girard’s granularity of proof-nets but on the level of terms. We also show some fundamental properties of the calculus such as confluence, strong normalization, preservation of β-strong normalization and the existence of a strong bisimulation that captures pairs of pn-terms having the same graph reduction.
Why Are Proofs Relevant in Proof-Relevant Models? Kerinec, Axel; Manzonetto, Giulio; Olimpieri, Federico
Proceedings of ACM on programming languages,
01/2023, Volume:
7, Issue:
POPL
Journal Article
Peer reviewed
Open access
Relational models of λ-calculus can be presented as type systems, the relational interpretation of a λ-term being given by the set of its typings. Within a distributors-induced bicategorical ...semantics generalizing the relational one, we identify the class of ‘categorified’ graph models and show that they can be presented as type systems as well. We prove that all the models living in this class satisfy an Approximation Theorem stating that the interpretation of a program corresponds to the filtered colimit of the denotations of its approximants. As in the relational case, the quantitative nature of our models allows to prove this property via a simple induction, rather than using impredicative techniques. Unlike relational models, our 2-dimensional graph models are also proof-relevant in the sense that the interpretation of a λ-term does not contain only its typings, but the whole type derivations. The additional information carried by a type derivation permits to reconstruct an approximant having the same type in the same environment. From this, we obtain the characterization of the theory induced by the categorified graph models as a simple corollary of the Approximation Theorem: two λ-terms have isomorphic interpretations exactly when their B'ohm trees coincide.
PDF
