scholarly journals Higher-Order Approximate Relational Refinement Types for Mechanism Design and Differential Privacy

2015 ◽  
Vol 50 (1) ◽  
pp. 55-68 ◽  
Author(s):  
Gilles Barthe ◽  
Marco Gaboardi ◽  
Emilio Jesús Gallego Arias ◽  
Justin Hsu ◽  
Aaron Roth ◽  
...  
Keyword(s):  
Mechanism Design ◽  
Differential Privacy ◽  
Higher Order ◽  
Refinement Types

scholarly journals Mechanism Design in Large Games: Incentives and Privacy

2014 ◽  
Vol 104 (5) ◽  
pp. 431-435 ◽  
Author(s):  
Michael Kearns ◽  
Mallesh M. Pai ◽  
Aaron Roth ◽  
Jonathan Ullman
Keyword(s):  
Mechanism Design ◽  
Differential Privacy ◽  
Additional Cost ◽  
Large Games ◽  
Privacy Concerns

We study the design of mechanisms satisfying a novel desideratum: privacy. This requires the mechanism not reveal 'much' about any agent's type to other agents. We propose the notion of joint differential privacy: a variant of differential privacy used in the privacy literature. We show by construction that mechanisms satisfying our desiderata exist when there are a large number of players, and any player's action affects any other's payoff by at most a small amount. Our results imply that in large economies, privacy concerns of agents can be accommodated at no additional 'cost' to standard incentive concerns.

scholarly journals Duet: an expressive higher-order language and linear type system for statically enforcing differential privacy

2019 ◽  
Vol 3 (OOPSLA) ◽  
pp. 1-30 ◽  
Author(s):  
Joseph P. Near ◽  
David Darais ◽  
Chike Abuah ◽  
Tim Stevens ◽  
Pranav Gaddamadugu ◽  
...  
Keyword(s):  
Differential Privacy ◽  
Type System ◽  
Higher Order ◽  
Linear Type ◽  
Order Language

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.

Sign in / Sign up

Export Citation Format

Share Document