Dependent types and multi-monadic effects in F*

DOI10.1145/2837614.2837655zbMath1347.68038OpenAlexW2267469130MaRDI QIDQ2828265

Santiago Zanella Béguelin, Aseem Rastogi, Antoine Delignat-Lavaud, Pierre-Yves Strub, Nikhil Swamy, Cătălin Hriţcu, Jean-Karim Zinzindohoue, Markulf Kohlweiss, Karthikeyan Bhargavan, Simon Forest, Chantal Keller, Cédric Fournet

Publication date: 24 October 2016

Published in: Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1145/2837614.2837655

zbMATH Keywords

verificationproof assistantseffectful programming

Mathematics Subject Classification ID

Related Items (10)

ConSORT: Context- and Flow-Sensitive Ownership Refinement Types for Imperative Programs ⋮ Short variable length domain extenders with beyond birthday bound security ⋮ A tutorial-style introduction to \(\mathsf{DY}^{\star}\) ⋮ State separation for code-based game-playing proofs ⋮ Unnamed Item ⋮ Verified Characteristic Formulae for CakeML ⋮ Modular Verification of Higher-Order Functional Programs ⋮ Deniable Functional Encryption ⋮ Automatic proofs of memory deallocation for a Whiley-to-C compiler ⋮ Ready,Set, Verify! Applyinghs-to-coqto real-world Haskell code

Uses Software

• Coq
• Haskell
• Why3
• OCaml
• foetus
• Autosubst

This page was built for publication: Dependent types and multi-monadic effects in F*