Subscribe to the gold package and get unlimited access to Shamra Academy
Register a new userTyped Closure Conversion for the Calculus of Constructions
172
0
0.0
(
0
)
Added by
William J. Bowman
Publication date
2018
fields
Informatics Engineering
and research's language is
English
Ask ChatGPT about the research
No Arabic abstract
Dependently typed languages such as Coq are used to specify and verify the full functional correctness of source programs. Type-preserving compilation can be used to preserve these specifications and proofs of correctness through compilation into the generated target-language programs. Unfortunately, type-preserving compilation of dependent types is hard. In essence, the problem is that dependent type systems are designed around high-level compositional abstractions to decide type checking, but compilation interferes with the type-system rules for reasoning about run-time terms. We develop a type-preserving closure-conversion translation from the Calculus of Constructions (CC) with strong dependent pairs ($Sigma$ types)---a subset of the core language of Coq---to a type-safe, dependently typed compiler intermediate language named CC-CC. The central challenge in this work is how to translate the source type-system rules for reasoning about functions into target type-system rules for reasoning about closures. To justify these rules, we prove soundness of CC-CC by giving a model in CC. In addition to type preservation, we prove correctness of separate compilation.
rate research
Read More
We study a dependently typed extension of a multi-stage programming language `a la MetaOCaml, which supports quasi-quotation and cross-stage persistence for manipulation of code fragments as first-class values and an evaluation construct for execution of programs dynamically generated by this code manipulation. Dependent types are expected to bring to multi-stage programming enforcement of strong invariant -- beyond simple type safety -- on the behavior of dynamically generated code. An extension is, however, not trivial because such a type system would have to take stages of types -- roughly speaking, the number of surrounding quotations -- into account. To rigorously study properties of such an extension, we develop $lambda^{MD}$, which is an extension of Hanada and Igarashis typed calculus $lambda^{triangleright%} $ with dependent types, and prove its properties including preservation, confluence, strong normalization for full reduction, and progress for staged reduction. Motivated by code generators that generate code whose type depends on a value from outside of the quotations, we argue the significance of cross-stage persistence in dependently typed multi-stage programming and certain type equivalences that are not directly derived from reduction rules.
The polymorphic RPC calculus allows programmers to write succinct multitier programs using polymorphic location constructs. However, until now it lacked an implementation. We develop an experimental programming language based on the polymorphic RPC calculus. We introduce a polymorphic Client-Server (CS) calculus with the client and server parts separated. In contrast to existing untyped CS calculi, our calculus is not only able to resolve polymorphic locations statically, but it is also able to do so dynamically. We design a type-based slicing compilation of the polymorphic RPC calculus into this CS calculus, proving type and semantic correctness. We propose a method to erase types unnecessary for execution but retaining locations at runtime by translating the polymorphic CS calculus into an untyped CS calculus, proving semantic correctness.
Safely integrating third-party code in applications while protecting the confidentiality of information is a long-standing problem. Pure functional programming languages, like Haskell, make it possible to enforce lightweight information-flow control through libraries like MAC by Russo. This work presents DepSec, a MAC inspired, dependently typed library for static information-flow control in Idris. We showcase how adding dependent types increases the expressiveness of state-of-the-art static information-flow control libraries and how DepSec matches a special-purpose dependent information-flow type system on a key example. Finally, we show novel and powerful means of specifying statically enforced declassification policies using dependent types.
Provenance is an increasing concern due to the ongoing revolution in sharing and processing scientific data on the Web and in other computer systems. It is proposed that many computer systems will need to become provenance-aware in order to provide satisfactory accountability, reproducibility, and trust for scientific or other high-value data. To date, there is not a consensus concerning appropriate formal models or security properties for provenance. In previous work, we introduced a formal framework for provenance security and proposed formal definitions of properties called disclosure and obfuscation. In this article, we study refined notions of positive and negative disclosure and obfuscation in a concrete setting, that of a general-purpose programing language. Previous models of provenance have focused on special-purpose languages such as workflows and database queries. We consider a higher-order, functional language with sums, products, and recursive types and functions, and equip it with a tracing semantics in which traces themselves can be replayed as computations. We present an annotation-propagation framework that supports many provenance views over traces, including standard forms of provenance studied previously. We investigate some relationships among provenance views and develop some partial solutions to the disclosure and obfuscation problems, including correct algorithms for disclosure and positive obfuscation based on trace slicing.
We introduce a new diagrammatic notation for representing the result of (algebraic) effectful computations. Our notation explicitly separates the effects produced during a computation from the possible values returned, this way simplifying the extension of definitions and results on pure computations to an effectful setting. Additionally, we show a number of algebraic and order-theoretic laws on diagrams, this way laying the foundations for a diagrammatic calculus of algebraic effects. We give a formal foundation for such a calculus in terms of Lawvere theories and generic effects.
Log in to be able to interact and post comments
comments
Fetching comments
Sign in to be able to follow your search criteria
