Dependent types and multi-monadic effects in F^*
DOI10.1145/2837614.2837655zbMATH Open1347.68038OpenAlexW2267469130MaRDI QIDQ2828265FDOQ2828265
Santiago Zanella-Béguelin, Aseem Rastogi, Antoine Delignat-Lavaud, Cédric Fournet, Pierre-Yves Strub, Nikhil Swamy, Cătălin Hriţcu, Jean-Karim Zinzindohoue, Markulf Kohlweiss, Karthikeyan Bhargavan, Simon Forest, Chantal Keller
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
Cited In (13)
- Ready,Set, Verify! Applyinghs-to-coqto real-world Haskell code
- ConSORT: Context- and Flow-Sensitive Ownership Refinement Types for Imperative Programs
- L ax F: Side Conditions and External Evidence as Monads
- Signature restriction for polymorphic algebraic effects
- Short variable length domain extenders with beyond birthday bound security
- State separation for code-based game-playing proofs
- Identifying overly restrictive matching patterns in SMT-based program verifiers (extended version)
- Verified Characteristic Formulae for CakeML
- A tutorial-style introduction to \(\mathsf{DY}^{\star}\)
- Deniable Functional Encryption
- Automatic proofs of memory deallocation for a Whiley-to-C compiler
- Title not available (Why is that?)
- Modular Verification of Higher-Order Functional Programs
Uses Software
This page was built for publication: Dependent types and multi-monadic effects in \(\mathrm{F}^*\)
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2828265)
