17 citations · 24 across the 5 of their papers we have counts for
5 papers
Foundational Verification of Smart Contracts through Verified Compilation
Vilhelm Sjöberg, Kinnari Dave, Daniel Britten +6
Programs executed on a blockchain - smart contracts - have high financial stakes; their correctness is crucial. We argue, that this correctness needs to be foundational: correctnes…
Irrelevance, Heterogeneous Equality, and Call-by-value Dependent Type Systems
Vilhelm Sjöberg, Chris Casinghino, Ki Yung Ahn +7
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 studi…
Step-Indexed Normalization for a Language with General Recursion
Chris Casinghino, Vilhelm Sjöberg, Stephanie Weirich
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 normal…
Equality, Quasi-Implicit Products, and Large Eliminations
Vilhelm Sjöberg, Aaron Stump
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 impli…
Termination Casts: A Flexible Approach to Termination with General Recursion
Aaron Stump, Vilhelm Sjöberg, Stephanie Weirich
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 lambd…