Dependent types and multi-monadic effects in F^*
DOI10.1145/2837614.2837655zbMATH Open1347.68038OpenAlexW2267469130MaRDI QIDQ2828265FDOQ2828265
Authors: Nikhil Swamy, Cătălin Hriţcu, Chantal Keller, Aseem Rastogi, Antoine Delignat-Lavaud, Simon Forest, Karthikeyan Bhargavan, Pierre-Yves Strub, Markulf Kohlweiss, Jean-Karim Zinzindohoue, Santiago Zanella-Béguelin, 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
Recommendations
Cited In (22)
- Self-certification: bootstrapping certified typecheckers in F\(^\ast\) with Coq
- \textit{Re}\(\mathcal{Q}\)\textsc{wire}: reasoning about reversible quantum circuits
- Verified characteristic formulae for CakeML
- L ax F: Side Conditions and External Evidence as Monads
- Context dependent procedures and computed types in \texttt{VeriFun}
- Signature restriction for polymorphic algebraic effects
- Short variable length domain extenders with beyond birthday bound security
- Modular verification of programs with effects and effect handlers in Coq
- State separation for code-based game-playing proofs
- Identifying overly restrictive matching patterns in SMT-based program verifiers (extended version)
- Ready, set, verify! Applying hs-to-coq to real-world Haskell code
- A tutorial-style introduction to \(\mathsf{DY}^{\star}\)
- Deniable Functional Encryption
- ConSORT: context- and flow-sensitive ownership refinement types for imperative programs
- Secure distributed programming with value-dependent types
- Secure distributed programming with value-dependent types
- Automatic proofs of memory deallocation for a Whiley-to-C compiler
- Meta-F\textsuperscript{\(\star\)}: proof automation with SMT, tactics, and metaprograms
- Modular verification of higher-order functional programs
- An intrinsic encoding of a subset of C and its application to TLS network packet processing
- Ynot: dependent types for imperative programs
- Dijkstra monads for free
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)
