Combining higher-order abstract syntax and (co)induction in a logical framework is well known to be problematic. Previous work described the implementation of a tool called Hybrid, within Isabelle HOL, which aims to address many of these difficulties. It allows object logics to be represented using higher-order abstract syntax, and reasoned about using tactical theorem proving and principles of (co)induction. In this paper we describe how to use it in a multi-level reasoning fashion, similar in spirit to other meta-logics such as Twelf. By explicitly referencing provability in a middle layer called a specification logic, we solve the problem of reasoning by (co)induction in the presence of non-stratifiable hypothetical judgments, which allow very elegant and succinct specifications of object logic inference rules.
This article responds to a critique of higher-order abstract syntax appearing in Logic Column 14, ``Nominal Logic and Abstract Syntax'', cs.LO/0511025.
Nominal abstract syntax and higher-order abstract syntax provide a means for describing binding structure which is higher-level than traditional techniques. These approaches have spawned two different communities which have developed along similar lines but with subtle differences that make them difficult to relate. The nominal abstract syntax community has devices like names, freshness, name-abstractions with variable capture, and the new-quantifier, whereas the higher-order abstract syntax community has devices like lambda-binders, lambda-conversion, raising, and the nabla-quantifier. This p…
Formalizing syntactic proofs of properties of logics, programming languages, security protocols, and other formal systems is a significant challenge, in large part because of the obligation to handle name-binding correctly. We present an approach called nominal abstract syntax that has attracted considerable interest since its introduction approximately six years ago. After an overview of other approaches, we describe nominal abstract syntax and nominal logic, a logic for reasoning about nominal abstract syntax. We also discuss applications of nominal techniques to programming, automated reaso…
The notion of term graph encodes a refinement of inductively generated syntax in which regard is paid to the the sharing and discard of subterms. Inductively generated syntax has an abstract expression in terms of initial algebras for certain endofunctors on the category of sets, which permits one to go beyond the set-based case, and speak of inductively generated syntax in other settings. In this paper we give a similar abstract expression to the notion of term graph. Aspects of the concrete theory are redeveloped in this setting, and applications beyond the realm of sets discussed.
The contribution of this paper is the development of the syntax and semantics of multi-sorted nominal abstract binding trees (abts), an extension of second order universal algebra to support symbol-indexed families of operators. Nominal abts are essential for correctly treating the syntax of languages with generative phenomena, including exceptions and mutable state. Additionally we have developed the categorical semantics for abstract binding trees formally in Constructive Type Theory using the Agda proof assistant. Multi-sorted nominal abts also form the syntactic basis for the upcoming vers…
A variety of logical frameworks support the use of higher-order abstract syntax (HOAS) in representing formal systems. Although these systems seem superficially the same, they differ in a variety of ways; for example, how they handle a context of assumptions and which theorems about a given formal system can be concisely expressed and proved. Our contributions in this paper are three-fold: 1) we develop a common infrastructure for representing benchmarks for systems supporting reasoning with binders, 2) we present several concrete benchmarks, which highlight a variety of different aspects of r…
Initial Semantics aims at interpreting the syntax associated to a signature as the initial object of some category of 'models', yielding induction and recursion principles for abstract syntax. Zsidó proves an initiality result for simply-typed syntax: given a signature S, the abstract syntax associated to S constitutes the initial object in a category of models of S in monads. However, the iteration principle her theorem provides only accounts for translations between two languages over a fixed set of object types. We generalize Zsidó's notion of model such that object types may vary, yielding…
Abstract predicates are considered in this paper as abstraction technique for heap-separated configurations, and as genuine Prolog predicates which are translated straight into a corresponding formal language grammar used as validation scheme for intermediate heap states. The approach presented is rule-based because the abstract predicates are rule-based, the parsing technique can be interpreted as an automated fold/unfold of the corresponding heap graph.
Cedille is a relatively recent tool based on a Curry-style pure type theory, without a primitive datatype system. Using novel techniques based on dependent intersection types, inductive datatypes with their induction principles are derived. One benefit of this approach is that it allows exploration of new or advanced forms of inductive datatypes. This paper reports work in progress on one such form, namely higher-order abstract syntax (HOAS). We consider the nature of HOAS in the setting of pure type theory, comparing with the traditional concept of environment models for lambda calculus. We s…
We describe an approach to the verified implementation of transformations on functional programs that exploits the higher-order representation of syntax. In this approach, transformations are specified using the logic of hereditary Harrop formulas. On the one hand, these specifications serve directly as implementations, being programs in the language Lambda Prolog. On the other hand, they can be used as input to the Abella system which allows us to prove properties about them and thereby about the implementations. We argue that this approach is especially effective in realizing transformations…
Logical frameworks based on intuitionistic or linear logics with higher-type quantification have been successfully used to give high-level, modular, and formal specifications of many important judgments in the area of programming languages and inference systems. Given such specifications, it is natural to consider proving properties about the specified systems in the framework: for example, given the specification of evaluation for a functional programming language, prove that the language is deterministic or that evaluation preserves types. One challenge in developing a framework for such rea…
It is often useful, if not necessary, to reason about the syntactic structure of an expression in an interpreted language (i.e., a language with a semantics). This paper introduces a mathematical structure called a syntax framework that is intended to be an abstract model of a system for reasoning about the syntax of an interpreted language. Like many concrete systems for reasoning about syntax, a syntax framework contains a mapping of expressions in the interpreted language to syntactic values that represent the syntactic structures of the expressions; a language for reasoning about the synta…
Despite extensive research both on the theoretical and practical fronts, formalising, reasoning about, and implementing languages with variable binding is still a daunting endeavour - repetitive boilerplate and the overly complicated metatheory of capture-avoiding substitution often get in the way of progressing on to the actually interesting properties of a language. Existing developments offer some relief, however at the expense of inconvenient and error-prone term encodings and lack of formal foundations. We present a mathematically-inspired language-formalisation framework implemented in A…
We argue that the implementation and verification of compilers for functional programming languages are greatly simplified by employing a higher-order representation of syntax known as Higher-Order Abstract Syntax or HOAS. The underlying idea of HOAS is to use a meta-language that provides a built-in and logical treatment of binding related notions. By embedding the meta-language within a larger programming or reasoning framework, it is possible to absorb the treatment of binding structure in the object language into the meta-theory of the system, thereby greatly simplifying the overall implem…
Some personal recollections on the introduction of `abstract proof systems' as a framework for formulating syntax-independent, general results about rule derivability and admissibility. With a particular eye on the inspiration I owe to Roel de Vrijer: the analogy with abstract rewriting systems.
Evaluating higher-order functional programs through abstract machines inspired by the geometry of the interaction is known to induce $\textit{space}$ efficiencies, the price being $\textit{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 \emph{general} this phenomenon is, and how far the inefficiencies can go, in the worst case. We answer these questions formulating four different well-known ab…
Hybrid is a formal theory implemented in Isabelle/HOL that provides an interface for representing and reasoning about object languages using higher-order abstract syntax (HOAS). This interface is built around an HOAS variable-binding operator that is constructed definitionally from a de Bruijn index representation. In this paper we make a variety of improvements to Hybrid, culminating in an abstract interface that on one hand makes Hybrid a more mathematically satisfactory theory, and on the other hand has important practical benefits. We start with a modification of Hybrid's type of terms tha…
We extend our approach to abstract syntax (with binding constructions) through modules and linearity. First we give a new general definition of arity, yielding the companion notion of signature. Then we obtain a modularity result as requested by Ghani and Uustalu (2003): in our setting, merging two extensions of syntax corresponds to building an amalgamated sum. Finally we define a natural notion of equation concerning a signature and prove the existence of an initial semantics for a so-called representable signature equipped with a set of equations.
Algorithms like those for differentiating functional expressions manipulate the syntactic structure of mathematical expressions in a mathematically meaningful way. A formalization of such an algorithm should include a specification of its computational behavior, a specification of its mathematical meaning, and a mechanism for applying the algorithm to actual expressions. Achieving these goals requires the ability to integrate reasoning about the syntax of the expressions with reasoning about what the expressions mean. A syntax framework is a mathematical structure that is an abstract model for…
This paper investigates the use of symmetric monoidal closed (SMC) structure for representing syntax with variable binding, in particular for languages with linear aspects. In our setting, one first specifies an SMC theory T, which may express binding operations, in a way reminiscent from higher-order abstract syntax. This theory generates an SMC category S(T) whose morphisms are, in a sense, terms in the desired syntax. We apply our approach to Jensen and Milner's (abstract binding) bigraphs, which are linear w.r.t. processes. This leads to an alternative category of bigraphs, which we compar…
The definition is a common form of human expert knowledge, a building block of formal science and mathematics, a foundation for database theory and is supported in various forms in many knowledge representation and formal specification languages and systems. This paper is a formal study of some of the most common forms of inductive definitions found in scientific text: monotone inductive definition, definition by induction over a well-founded order and iterated inductive definitions. We define a logic of definitions offering a uniform formal syntax to express definitions of the different sorts…
In this thesis we give an algebraic characterization of the syntax and semantics of simply-typed languages. More precisely, we characterize simply-typed binding syntax equipped with reduction rules via a universal property, namely as the initial object of some category. We specify a language by a 2-signature (Σ, A), that is, a signature on two levels: the syntactic level Σ specifies the sorts and terms of the language, and associates a sort to each term. The semantic level A specifies, through inequations, reduction rules on the terms of the language. To any given 2-signature (Σ, A) we associa…
I introduce renaming-enriched sets (rensets for short), which are algebraic structures axiomatizing fundamental properties of renaming (also known as variable-for-variable substitution) on syntax with bindings. Rensets compare favorably in some respects with the well-known foundation based on nominal sets. In particular, renaming is a more fundamental operator than the nominal swapping operator and enjoys a simpler, equationally expressed relationship with the variable freshness predicate. Together with some natural axioms matching properties of the syntactic constructors, rensets yield a trul…
We have previously published the Isabelle/HOL formalization of a general theory of syntax with bindings. In this companion paper, we instantiate the general theory to the syntax of lambda-calculus and formalize the development leading to several fundamental constructions and results: sound semantic interpretation, the Church-Rosser and standardization theorems, and higher-order abstract syntax (HOAS) encoding. For Church-Rosser and standardization, our work covers both the call-by-name and call-by-value versions of the calculus, following classic papers by Takahashi and Plotkin. During the for…
Regular logic can be regarded as the internal language of regular categories, but the logic itself is generally not given a categorical treatment. In this paper, we understand the syntax and proof rules of regular logic in terms of the free regular category FRg(T) on a set T. From this point of view, regular theories are certain monoidal 2-functors from a suitable 2-category of contexts -- the 2-category of relations in FRg(T) -- to that of posets. Such functors assign to each context the set of formulas in that context, ordered by entailment. We refer to such a 2-functor as a regular calculus…
Abstract Compilation as Abstraction of Operator Semantics, applied to Cost Analysis
Universidad Politécnica de Madrid（马德里理工大学）；IMDEA Software Institute（IMDEA软件研究所）；Spanish Council for Scientific Research (CSIC)（西班牙国家研究委员会）；Computer Science Laboratory of Sorbonne University (LIP6)（索邦大学计算机科学实验室）；STMicroelectronics（意法半导体）
Initial Semantics aims at characterizing the syntax associated to a signature as the initial object of some category. We present an initial semantics result for typed higher-order syntax together with its formalization in the Coq proof assistant. The main theorem was first proved on paper in the second author's PhD thesis in 2010, and verified formally shortly afterwards. To a simply-typed binding signature S over a fixed set T of object types we associate a category called the category of representations of S. We show that this category has an initial object Sigma(S). From its construction it…
We present Hindley-Milner-Cousots (HMC), an algorithm that allows any interprocedural analysis for first-order imperative programs to be used to verify safety properties of typed higher-order functional programs. HMC works as follows. First, it uses the type structure of the functional program to generate a set of logical refinement constraints whose satisfaction implies the safety of the source program. Next, it transforms the logical refinement constraints into a simple first-order imperative program that is safe iff the constraints are satisfiable. Thus, in one swoop, HMC makes tools for in…
University of Corunna（拉科鲁尼亚大学）；University of Potsdam（波茨坦大学）
Characterizing hybrid ASP solving in a generic way is difficult since one needs to abstract from specific theories. Inspired by lazy SMT solving, this is usually addressed by treating theory atoms as opaque. Unlike this, we propose a slightly more transparent approach that includes an abstract notion of a term. Rather than imposing a syntax on terms, we keep them abstract by stipulating only some basic properties. With this, we further develop a semantic framework for hybrid ASP solving and provide aggregate functions for theory variables that adhere to different semantic principles, show that…
