scholarly journals ConSORT: Context- and Flow-Sensitive Ownership Refinement Types for Imperative Programs

2020 ◽  
pp. 684-714 ◽  
Author(s):  
John Toman ◽  
Ren Siqi ◽  
Kohei Suenaga ◽  
Atsushi Igarashi ◽  
Naoki Kobayashi
Keyword(s):  
Data Structure ◽  
Type System ◽  
Program Execution ◽  
Safety Verification ◽  
Refinement Types ◽  
Fractional Ownership ◽  
Automated Inference ◽  
Ownership Types

AbstractWe present ConSORT, a type system for safety verification in the presence of mutability and aliasing. Mutability requires strong updates to model changing invariants during program execution, but aliasing between pointers makes it difficult to determine which invariants must be updated in response to mutation. Our type system addresses this difficulty with a novel combination of refinement types and fractional ownership types. Fractional ownership types provide flow-sensitive and precise aliasing information for reference variables. ConSORT interprets this ownership information to soundly handle strong updates of potentially aliased references. We have proved ConSORT sound and implemented a prototype, fully automated inference tool. We evaluated our tool and found it verifies non-trivial programs including data structure implementations.

The essence of ornaments

2017 ◽  
Vol 27 ◽  
Author(s):  
PIERRE-EVARISTE DAGAND
Keyword(s):  
First Principles ◽  
Type System ◽  
Abstract Model ◽  
Inductive Definitions ◽  
Refinement Types ◽  
Definition Of ◽  
Do So ◽  
Program Invariants

AbstractFunctional programmers from all horizons strive to use, and sometimes abuse, their favorite type system in order to capture the invariants of their programs. A widely used tool in that trade consists in defining finely indexed datatypes. Operationally, these types classify the programmer's data, following the ML tradition. Logically, these types enforce the program invariants in a novel manner. This new programming pattern, by which one programs over inductive definitions to account for some invariants, lead to the development of a theory of ornaments (McBride, 2011 Ornamental Algebras, Algebraic Ornaments. Unpublished). However, ornaments originate as a dependently-typed object and may thus appear rather daunting to a functional programmer of the non-dependent kind. This article aims at presenting ornaments from first-principles and, in particular, to declutter their presentation from syntactic considerations. To do so, we shall give a sufficiently abstract model of indexed datatypes by means of many-sorted signatures. In this process, we formalize our intuition that an indexed datatype is the combination of a data-structure and a data-logic. Over this abstraction of datatypes, we shall recast the definition of ornaments, effectively giving a model of ornaments. Benefiting both from the operational and abstract nature of many-sorted signatures, ornaments should appear applicable and, one hopes, of interest beyond the type-theoretic circles, case in point being languages with generalized abstract datatypes or refinement types.

scholarly journals Object Cloning for Ownership Systems

2021 ◽  
Author(s):  
◽  
Paley Guangping Li
Keyword(s):  
Comparative Analysis ◽  
Programming Languages ◽  
Formal Model ◽  
Operational Semantics ◽  
Type System ◽  
Object Oriented ◽  
Object Oriented Programming ◽  
Constraint System ◽  
Existential Quantification ◽  
Ownership Types

<p>Modern object-oriented programming languages frequently need the ability to clone, duplicate, and copy objects. The usual approaches taken by languages are rudimentary, primarily because these approaches operate with little understanding of the object being cloned. Deep cloning naively copies every object that has a reachable reference path from the object being cloned, even if the objects being copied have no innate relationship with that object. For more sophisticated cloning operations, languages usually only provide the capacity for programmers to define their own cloning operations for specific objects, and with no help from the type system.  Sheep cloning is an automated operation that clones objects by leveraging information about those objects’ structures, which the programmer imparts into their programs with ownership types. Ownership types are a language mechanism that defines an owner for every object in the program. Ownership types create a hierarchical structure for the heap.  In this thesis, we construct an extensible formal model for an object-oriented language with ownership types (Core), and use it to explore different formalisms of sheep cloning. We formalise three distinct operational semantics of sheep cloning, and for each approach we include proofs or proof outlines where appropriate, and provide a comparative analysis of each model’s benefits. Our main contribution is the descripSC formal model of sheep cloning and its proof of type soundness.  The second contribution of this thesis is the formalism of Mojo-jojo, a multiple ownership system that includes existential quantification over types and context parameters, along with a constraint system for context parameters. We prove type soundness for Mojo-jojo. Multiple ownership is a mechanism which allows objects to have more than one owner. Context parameters in Mojo-jojo can use binary operators such as: intersection, union, and disjointness.</p>

scholarly journals Practical run-time checking via unobtrusive property caching

2015 ◽  
Vol 15 (4-5) ◽  
pp. 726-741 ◽  
Author(s):  
NATALIIA STULOVA ◽  
JOSÉ F. MORALES ◽  
MANUEL V. HERMENEGILDO
Keyword(s):  
Data Structure ◽  
Operational Semantics ◽  
Experimental Results ◽  
High Time ◽  
Program Execution ◽  
Structure Representation ◽  
Prototype Implementation ◽  
Standard Program ◽  
Dynamic Programing ◽  
Run Time

AbstractThe use of annotations, referred to as assertions or contracts, to describe program properties for which run-time tests are to be generated, has become frequent in dynamic programing languages. However, the frameworks proposed to support such run-time testing generally incur high time and/or space overheads over standard program execution. We present an approach for reducing this overhead that is based on the use of memoization to cache intermediate results of check evaluation, avoiding repeated checking of previously verified properties. Compared to approaches that reduce checking frequency, our proposal has the advantage of being exhaustive (i.e., all tests are checked at all points) while still being much more efficient than standard run-time checking. Compared to the limited previous work on memoization, it performs the task without requiring modifications to data structure representation or checking code. While the approach is general and system-independent, we present it for concreteness in the context of the Ciao run-time checking framework, which allows us to provide an operational semantics with checks and caching. We also report on a prototype implementation and provide some experimental results that support that using a relatively small cache leads to significant decreases in run-time checking overhead.

scholarly journals Data Structures in Leelus Programming Language: A Research

2021 ◽  
Author(s):  
Frank Appiah
Keyword(s):  
Data Structure ◽  
Programming Language ◽  
Data Structures ◽  
Type System

This is a research on data structures using pointer declaration for array dimensional type of representation in variable declaration. In this research, I will describe type array, term array and value array drawn from both data structure and type system.

scholarly journals A certified lightweight non-interference Java bytecode verifier

2013 ◽  
Vol 23 (5) ◽  
pp. 1032-1081 ◽  
Author(s):  
GILLES BARTHE ◽  
DAVID PICHARDIE ◽  
TAMARA REZK
Keyword(s):  
Programming Languages ◽  
Information Flow ◽  
Type System ◽  
Type Systems ◽  
Program Execution ◽  
Flow Type ◽  
Java Bytecode ◽  
First Sound ◽  
Coq Proof Assistant ◽  
High Level

Non-interference guarantees the absence of illicit information flow throughout program execution. It can be enforced by appropriate information flow type systems. Much of the previous work on type systems for non-interference has focused on calculi or high-level programming languages, and existing type systems for low-level languages typically omit objects, exceptions and method calls. We define an information flow type system for a sequential JVM-like language that includes all these programming features, and we prove, in the Coq proof assistant, that it guarantees non-interference. An additional benefit of the formalisation is that we have extracted from our proof a certified lightweight bytecode verifier for information flow. Our work provides, to the best of our knowledge, the first sound and certified information flow type system for such an expressive fragment of the JVM.

Contracts made manifest

2012 ◽  
Vol 22 (3) ◽  
pp. 225-274 ◽  
Author(s):  
MICHAEL GREENBERG ◽  
BENJAMIN C. PIERCE ◽  
STEPHANIE WEIRICH
Keyword(s):  
Type System ◽  
Higher Order ◽  
The Other ◽  
Simple Type ◽  
Free Variables ◽  
Refinement Types ◽  
Static Information ◽  
Analogous Theorem

AbstractSince Findler and Felleisen (Findler, R. B. & Felleisen, M. 2002) introduced higher-order contracts, many variants have been proposed. Broadly, these fall into two groups: some follow Findler and Felleisen (2002) in using latent contracts, purely dynamic checks that are transparent to the type system; others use manifest contracts, where refinement types record the most recent check that has been applied to each value. These two approaches are commonly assumed to be equivalent—different ways of implementing the same idea, one retaining a simple type system, and the other providing more static information. Our goal is to formalize and clarify this folklore understanding. Our work extends that of Gronski and Flanagan (Gronski, J. & Flanagan, C. 2007), who defined a latent calculus λC and a manifest calculus λH, gave a translation φ from λC to λH, and proved that if a λC term reduces to a constant, so does its φ-image. We enrich their account with a translation ψ from λH to λC and prove an analogous theorem. We then generalize the whole framework to dependent contracts, whose predicates can mention free variables. This extension is both pragmatically crucial, supporting a much more interesting range of contracts, and theoretically challenging. We define dependent versions of λH and two dialects (“lax” and “picky”) of λC, establish type soundness—a substantial result in itself, for λH — and extend φ and ψ accordingly. Surprisingly, the intuition that the latent and manifest systems are equivalent now breaks down: the extended translations preserve behavior in one direction, but in the other, sometimes yield terms that blame more.

scholarly journals Helmholtz: A Verifier for Tezos Smart Contracts Based on Refinement Types

2021 ◽  
pp. 262-280
Author(s):  
Yuki Nishida ◽  
Hiromasa Saito ◽  
Ran Chen ◽  
Akira Kawata ◽  
Jun Furuse ◽  
...  
Keyword(s):  
Type System ◽  
Higher Order ◽  
Smart Contracts ◽  
Static Verification ◽  
Smt Solver ◽  
The Core ◽  
Verification Conditions ◽  
Refinement Types ◽  
Characteristic Features ◽  
Higher Order Functions

AbstractA smart contract is a program executed on a blockchain, based on which many cryptocurrencies are implemented, and is being used for automating transactions. Due to the large amount of money that smart contracts deal with, there is a surging demand for a method that can statically and formally verify them.This tool paper describes our type-based static verification tool Helmholtz for Michelson, which is a statically typed stack-based language for writing smart contracts that are executed on the blockchain platform Tezos. Helmholtz is designed on top of our extension of Michelson’s type system with refinement types. Helmholtz takes a Michelson program annotated with a user-defined specification written in the form of a refinement type as input; it then typechecks the program against the specification based on the refinement type system, discharging the generated verification conditions with the SMT solver Z3. We briefly introduce our refinement type system for the core calculus Mini-Michelson of Michelson, which incorporates the characteristic features such as compound datatypes (e.g., lists and pairs), higher-order functions, and invocation of another contract. Helmholtz successfully verifies several practical Michelson programs, including one that transfers money to an account and that checks a digital signature.

scholarly journals Object Cloning for Ownership Systems

2021 ◽  
Author(s):  
◽  
Paley Guangping Li
Keyword(s):  
Comparative Analysis ◽  
Programming Languages ◽  
Formal Model ◽  
Operational Semantics ◽  
Type System ◽  
Object Oriented ◽  
Object Oriented Programming ◽  
Constraint System ◽  
Existential Quantification ◽  
Ownership Types

<p>Modern object-oriented programming languages frequently need the ability to clone, duplicate, and copy objects. The usual approaches taken by languages are rudimentary, primarily because these approaches operate with little understanding of the object being cloned. Deep cloning naively copies every object that has a reachable reference path from the object being cloned, even if the objects being copied have no innate relationship with that object. For more sophisticated cloning operations, languages usually only provide the capacity for programmers to define their own cloning operations for specific objects, and with no help from the type system.  Sheep cloning is an automated operation that clones objects by leveraging information about those objects’ structures, which the programmer imparts into their programs with ownership types. Ownership types are a language mechanism that defines an owner for every object in the program. Ownership types create a hierarchical structure for the heap.  In this thesis, we construct an extensible formal model for an object-oriented language with ownership types (Core), and use it to explore different formalisms of sheep cloning. We formalise three distinct operational semantics of sheep cloning, and for each approach we include proofs or proof outlines where appropriate, and provide a comparative analysis of each model’s benefits. Our main contribution is the descripSC formal model of sheep cloning and its proof of type soundness.  The second contribution of this thesis is the formalism of Mojo-jojo, a multiple ownership system that includes existential quantification over types and context parameters, along with a constraint system for context parameters. We prove type soundness for Mojo-jojo. Multiple ownership is a mechanism which allows objects to have more than one owner. Context parameters in Mojo-jojo can use binary operators such as: intersection, union, and disjointness.</p>

scholarly journals A General Semantic Construction of Dependent Refinement Type Systems, Categorically

2021 ◽  
pp. 406-426
Author(s):  
Satoshi Kura
Keyword(s):  
Predicate Logic ◽  
Sufficient Conditions ◽  
Type System ◽  
Type Systems ◽  
Functional Languages ◽  
Refinement Types ◽  
General Semantic

AbstractDependent refinement types are types equipped with predicates that specify preconditions and postconditions of underlying functional languages. We propose a general semantic construction of dependent refinement type systems from underlying type systems and predicate logic, that is, a construction of liftings of closed comprehension categories from given (underlying) closed comprehension categories and posetal fibrations for predicate logic. We give sufficient conditions to lift structures such as dependent products, dependent sums, computational effects, and recursion from the underlying type systems to dependent refinement type systems. We demonstrate the usage of our construction by giving semantics to a dependent refinement type system and proving soundness.

Ultrastructural characteristics of sporidia of Ustilago

1989 ◽  
Vol 47 ◽  
pp. 786-787
Author(s):  
Patricia N. Hackney
Keyword(s):  
Electron Microscope ◽  
Type System ◽  
Tube Formation ◽  
High Voltage Electron Microscopy ◽  
Voltage Electron ◽  
University Of Wisconsin ◽  
Transmission Electron ◽  
Ustilago Hordei ◽  
Silene Alba ◽  
The University

Ustilago hordei and Ustilago violacea are yeast-like basidiomycete pathogens ofHordeum vulgare and Silene alba respectively. The mating type system in both species of Ustilago is bipolar, with alleles, A,a, (U.hordei) and a1, a2 (U.violacea) at a single locus. Haploid sporidia maintain the asexual phase by budding, while the sexual phase is initiated by conjugation tube formation between the mating types during budding and conjugation.For observation of budding, sporidia were prepared by culturing the four types on YEG (yeast extract glucose) broth for 24 hours. After centrifugation at 5000g cells were either left unmated or mated in a1/a2,A/a combinations. The sporidia were then mixed 1:1 with 4% agar and the resulting 1mm cubes fixed in 8% gluteraldehyde and post fixed in osmium tetroxide. After dehydration and embedding cubes were thin sectioned with a LKB ultratome and photographed in a Zeiss 9s transmission electron microscope or in an AE1 electron microscope of MK11 1MEV at the High Voltage Electron Microscopy Center of the University of Wisconsin-Madison.

Sign in / Sign up

Export Citation Format

Share Document