Showing 1–5 of 5 results for author: Sjöberg, V

Foundational Verification of Smart Contracts through Verified Compilation

Authors: Vilhelm Sjöberg, Kinnari Dave, Daniel Britten, Maria A Schett, Xinyuan Sun, Qinshi Wang, Sean Noble Anderson, Steve Reeves, Zhong Shao

Abstract: Programs executed on a blockchain - smart contracts - have high financial stakes; their correctness is crucial. We argue, that this correctness needs to be foundational: correctness needs to be based on the operational semantics of their execution environment. In this work we present a foundational system - the DeepSEA system - targeting the Ethereum blockchain as the largest smart contract platfo… ▽ More Programs executed on a blockchain - smart contracts - have high financial stakes; their correctness is crucial. We argue, that this correctness needs to be foundational: correctness needs to be based on the operational semantics of their execution environment. In this work we present a foundational system - the DeepSEA system - targeting the Ethereum blockchain as the largest smart contract platform. The DeepSEA system has a small but sufficiently rich programming language amenable for verification, the DeepSEA language, and a verified DeepSEA compiler. Together they enable true end-to-end verification for smart contracts. We demonstrate usability through two case studies: a realistic contract for Decentralized Finance and contract for crowdfunding. △ Less

Submitted 14 May, 2024; originally announced May 2024.

Comments: 27 pages, 6 figures

ACM Class: F.3.1; F.3.2

Irrelevance, Heterogeneous Equality, and Call-by-value Dependent Type Systems

Authors: Vilhelm Sjöberg, Chris Casinghino, Ki Yung Ahn, Nathan Collins, Harley D. Eades III, Peng Fu, Garrin Kimmell, Tim Sheard, Aaron Stump, Stephanie Weirich

Abstract: We present a full-spectrum dependently typed core language which includes both nontermination and computational irrelevance (a.k.a. erasure), a combination which has not been studied before. The two features interact: to protect type safety we must be careful to only erase terminating expressions. Our language design is strongly influenced by the choice of CBV evaluation, and by our novel treatmen… ▽ More We present a full-spectrum dependently typed core language which includes both nontermination and computational irrelevance (a.k.a. erasure), a combination which has not been studied before. The two features interact: to protect type safety we must be careful to only erase terminating expressions. Our language design is strongly influenced by the choice of CBV evaluation, and by our novel treatment of propositional equality which has a heterogeneous, completely erased elimination form. △ Less

Submitted 13 February, 2012; originally announced February 2012.

Comments: In Proceedings MSFP 2012, arXiv:1202.2407

ACM Class: D.3.1

Journal ref: EPTCS 76, 2012, pp. 112-162

Step-Indexed Normalization for a Language with General Recursion

Authors: Chris Casinghino, Vilhelm Sjöberg, Stephanie Weirich

Abstract: The Trellys project has produced several designs for practical dependently typed languages. These languages are broken into two fragments-a_logical_fragment where every term normalizes and which is consistent when interpreted as a logic, and a_programmatic_fragment with general recursion and other convenient but unsound features. In this paper, we present a small example language in this style.… ▽ More The Trellys project has produced several designs for practical dependently typed languages. These languages are broken into two fragments-a_logical_fragment where every term normalizes and which is consistent when interpreted as a logic, and a_programmatic_fragment with general recursion and other convenient but unsound features. In this paper, we present a small example language in this style. Our design allows the programmer to explicitly mention and pass information between the two fragments. We show that this feature substantially complicates the metatheory and present a new technique, combining the traditional Girard-Tait method with step-indexed logical relations, which we use to show normalization for the logical fragment. △ Less

Submitted 13 February, 2012; originally announced February 2012.

Comments: In Proceedings MSFP 2012, arXiv:1202.2407

Journal ref: EPTCS 76, 2012, pp. 25-39

Equality, Quasi-Implicit Products, and Large Eliminations

Authors: Vilhelm Sjöberg, Aaron Stump

Abstract: This paper presents a type theory with a form of equality reflection: provable equalities can be used to coerce the type of a term. Coercions and other annotations, including implicit arguments, are dropped during reduction of terms. We develop the metatheory for an undecidable version of the system with unannotated terms. We then devise a decidable system with annotated terms, justified in term… ▽ More This paper presents a type theory with a form of equality reflection: provable equalities can be used to coerce the type of a term. Coercions and other annotations, including implicit arguments, are dropped during reduction of terms. We develop the metatheory for an undecidable version of the system with unannotated terms. We then devise a decidable system with annotated terms, justified in terms of the unannotated system. Finally, we show how the approach can be extended to account for large eliminations, using what we call quasi-implicit products. △ Less

Submitted 23 January, 2011; originally announced January 2011.

Comments: In Proceedings ITRS 2010, arXiv:1101.4104

ACM Class: D.3.1

Journal ref: EPTCS 45, 2011, pp. 90-100

Termination Casts: A Flexible Approach to Termination with General Recursion

Authors: Aaron Stump, Vilhelm Sjöberg, Stephanie Weirich

Abstract: This paper proposes a type-and-effect system called Teqt, which distinguishes terminating terms and total functions from possibly diverging terms and partial functions, for a lambda calculus with general recursion and equality types. The central idea is to include a primitive type-form "Terminates t", expressing that term t is terminating; and then allow terms t to be coerced from possibly diverg… ▽ More This paper proposes a type-and-effect system called Teqt, which distinguishes terminating terms and total functions from possibly diverging terms and partial functions, for a lambda calculus with general recursion and equality types. The central idea is to include a primitive type-form "Terminates t", expressing that term t is terminating; and then allow terms t to be coerced from possibly diverging to total, using a proof of Terminates t. We call such coercions termination casts, and show how to implement terminating recursion using them. For the meta-theory of the system, we describe a translation from Teqt to a logical theory of termination for general recursive, simply typed functions. Every ty** judgment of Teqt is translated to a theorem expressing the appropriate termination property of the computational part of the Teqt term. △ Less

Submitted 22 December, 2010; originally announced December 2010.

Comments: In Proceedings PAR 2010, arXiv:1012.4555

ACM Class: D.3.1

Journal ref: EPTCS 43, 2010, pp. 76-93