Dependent types and multi-monadic effects in F^*
From MaRDI portal
Publication:2828265
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}
- Short variable length domain extenders with beyond birthday bound security
- Signature restriction for polymorphic algebraic effects
- 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)
- A tutorial-style introduction to \(\mathsf{DY}^{\star}\)
- Deniable Functional Encryption
- Ready, set, verify! Applying hs-to-coq to real-world Haskell code
- 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
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)
