Dependent types and multi-monadic effects in F*

By Nikhil Swamy, Cătălin Hrițcu, C. Keller, Aseem Rastogi, Antoine Delignat-Lavaud, Simon Forest, Karthikeyan Bhargavan, Cédric Fournet, Pierre-Yves Strub, Markulf Kohlweiss and 2 more. ACM-SIGACT Symposium on Principles of Programming Languages, 2016

434 citations recorded by the source corpus.

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

An Overview on Smart Contracts: Challenges, Advances and Platforms (2019, neutral): “1) Contract correctness • Source code analysis [54], [55], [56], [57]”
A Survey of Attacks on Ethereum Smart Contracts (SoK) (2017, methodology): “The tool presented in [26] translates smart contracts, either Solidity or EVM bytecode, into the functional language F∗ [53].”
MaxSMT-Based Type Inference for Python 3 (2018, background): “Both F* [24] and LiquidHaskell [26] (partly) use SMT-solving in the inference for their dependent type systems.”
RustBelt: securing the foundations of the rust programming language (2017, result): “In a related but very different line of work, systems like Ynot [Nanevski et al. 2008], FCSL [Nanevski et al. 2014], and F ∗ [Swamy et al. 2016] integrate variants of separation logic into dependent type theory.”
Formal Verification of Smart Contracts: Short Paper (2016, methodology): “The base construction is a combined exception and state monad (see [9] for details) with the following signature:”