1,721,011 research outputs found
Mechanizing type environments in weak HOAS
Full text linkWe provide a paradigmatic case study, about the formalization of System F<:'s type language in the proof assistant Coq. Our approach relies on weak HOAS, for the sake of producing a readable and concise representation of the object language. Actually, we present and discuss two encoding strategies for typing environments which yield a remarkable influence on the whole formalization. Then, on the one hand we develop System F<:'s metatheory, on the other hand we address the equivalence of the two approaches internally to Coq
Internal Adequacy of Bookkeeping in Coq
No full textWe focus on a common problem encountered in encoding and formally reasoning about a wide range of formal systems, namely, the representation of a typing environment. In particular, we apply the bookkeeping technique to a well-known case study (i.e., System F<:'s type language), proving in Coq an internal correspondence with a more standard representation of the typing environment as a list of pairs. In order to keep the signature readable and concise, we make use of higher-order abstract syntax (HOAS), which allows us to deal smoothly with the representation of the universal binder of System F<: type language
Types for Proofs and Programs International Conference, TYPES 2007, Revised Selected Papers
No full textMobile Search Behaviors: An In-Depth Analysis Based on Contexts, APPs, and Devices. Dan Wu and Shaobo Liang. Synthesis Lectures on Information Concepts, Retrieval, and Services. San Rafael, CA: Morgan & Claypool, 2018. 159 pp. $51.96 (e-book). (ISBN 9781681733005)
No full text
A Framework for Typed HOAS and Semantics
No full textWe investigate a framework for representing and reasoning about syntactic and semantic aspects of typed languages with variable binders.First, we introduce typed binding signatures and develop a theory of typed abstract syntax with binders. Each signature is associated to a category of "presentation" models, where the language of the typed signature is the initial model.At the semantic level, types can be given also a computational meaning in a (possibly different) semantic category. We observe that in general, semantic aspects of terms and variables can be reflected in the presentation category by means of an adjunction. Therefore, the category of presentation models is expressive enough to represent both the syntactic and the semantic aspects of languages.We introduce then a metalogical system, inspired by the internal languages of the presentation category, which can be used for reasoning on both the syntax and the semantics of languages. This system is composed by a core equational logic tailored for reasoning on the syntactic aspects; when a specific semantics is chosen, the system can be modularly extended with further "semantic" notions, as needed
Plug and Play the Theory of Contexts in Higher-Order abstract Syntax
No full textWe illustrate the pragmatic aspects of the Theory of Contexts, recently proposed as a general approach for reasoning on languages with binders in Higher-Order Abstract Syntax, through two working examples: λ-calculus and Abadi and Cardelli’s impς-calculus
The Theory of Contexts for First Order and Higher Order Abstract Syntax
No full textWe present two case studies in formal reasoning about untyped λ-calculus in Coq, using both first-order and higher-order abstract syntax. In the first case, we prove the equivalence of three definitions of α-equivalence; in the second, we focus on properties of substitution. In both cases, we deal with contexts, which are rendered by means of higher-order terms (functions) in the metalanguage. These are successfully handled by using the Theory of Contexts
Logical Predicates as First-Class Citizens in LF
No full textThe Edinburgh Logical Framework LF was introduced both as a general theory of logics and as a metalanguage for a generic proof development environment. In this paper, we consider an extension of LF, called the Logical-Logical Framework LLF, that features predicates as first-class citizens that can be reified and passed as arguments, as a special kind of functional objects. These functional objects return the argument under the condition that it satisfies a logical predicate, or simply freeze the argument until this predicate becomes true. We study the language theory of LLF and provide proofs for subject reduction, confluence, and strong normalization. By way of example, we illustrate how special instances of LLF allow for encodings of side-conditions of Modal Logics in Hilbert style and a direct encoding of pre- and post-conditions on input and output of a theory of functions. Our motivation for introducing LLF is twofold. First, the type system of LF is too coarse with respect to the “side conditions” that it can enforce on the application of rules. Second, almost all logics are encodable in LF (with a greater or lesser degree of difficulty involved, depending on the choice of logic) but never participate actively in the reductions. This last point requires further attention: by the Curry-Howard isomorphism, types are formulæ (theorems) and λ-terms are logical proofs of the the validity of the formulæ (or the proof of the theorem). LLF moves the “periscope” of this 30- year-old principle onto another direction: λ-terms can also be formulæ the proof of which is not encoded in LLF itself but “externalized”, via an external call, to a logical system from which we request the verification of the truth of the formula itself. Following Curry-Howard, one can view this externalization as an “oracle call”, which will be typed with a suitable type representing the oracle itself.
Historically, the idea of having stuck-reduction in objects and types in the setting of higher-order term rewriting systems with sophisticated pattern-matching capabilities was first introduced in Cirstea-Kirchner-Liquori’s Rho-cube, in order to design a hierarchy of type systems for the untyped Rewriting Calculus, and was later generalized to a framework of Pure Type Systems with Patterns. This typing protocol was essential in the effort to preserve the strong normalization of typable terms. The idea underlying the Logical-Logical Framework LLF is the same as that exploit for the General Logical Framework GLF. However, there is an important difference between the two frameworks in the definition of predicates. Predicates in are used both to determine whether β-reduction fires and to compute a substitution, while in the present paper they are truly first-class objects. A further attempt was done with the Constrained Logical Framework CLF by the same authors. The big difference between the two frameworks is that reduction was typed in CLF, while it is untyped in LLF, and that CLF relies on an infinite number of binders λP , each of which encoded one logical predicate, while the predicates in LLF are first-class objects declared in contexts: this latter point has a direct fallback in the viewing of LLF as a kernel for proof assistants, since we do not need to “parse” the metalanguage each time we add a new predicate.
Apart from encodings of Modal Logics, we believe that our Logical-Logical Framework could also be very helpful in modeling dynamic and reactive systems: for example bio-inspired systems, where reactions of chemical processes take place only provided some extra structural or temporal conditions; or process algebras, where often no assumptions can be made about messages exchanged through the communication channels. Indeed, it could be the case that a redex, depending on the result of a communication, can remain stuck until a “good” message arrives from a given channel, firing in that case an appropriate reduction (this is a common situation in many protocols, where “bad” requests are ignored and “good ones” are served). Such dynamic (run-time) behaviour could hardly be captured by a rigid type discipline, where bad terms and hypotheses are ruled out a priori.
Another interesting improvement is to be found in proving program correctness. It is well known that encoding pre- and post-conditions in LF if not so obvious: nevertheless, despite the theoretical difficulty, and driven by the importance of writing code which can be proven to be “correct”, this decade has seen a plæthora of software tools bridging the gap between proof assistants and prototype programming languages, featuring built-in Hoare-logic-inspired primitives (such as the Why pre-compiler, translating pre- and post-condition annotations into Coq proof obligations). Having the possibility to externalize the call to logical systems via a simple term application greatly simplifies this task
- …
