Dependent types and multi-monadic effects in F^*
From MaRDI portal
Publication:2828265
Recommendations
Cited in
(29)- Short variable length domain extenders with beyond birthday bound security
- State separation for code-based game-playing proofs
- Modular verification of programs with effects and effect handlers in Coq
- Automatic proofs of memory deallocation for a Whiley-to-C compiler
- A tutorial-style introduction to \(\mathsf{DY}^{\star}\)
- Deniable Functional Encryption
- Context dependent procedures and computed types in \texttt{VeriFun}
- L ax F: Side Conditions and External Evidence as Monads
- Self-certification: bootstrapping certified typecheckers in F^ with Coq
- Verified characteristic formulae for CakeML
- Modular verification of higher-order functional programs
- \textit{Re}\(\mathcal{Q}\)\textsc{wire}: reasoning about reversible quantum circuits
- 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
- Ynot: dependent types for imperative programs
- An intrinsic encoding of a subset of C and its application to TLS network packet processing
- Dijkstra monads for free
- Secure distributed programming with value-dependent types
- Meta-F\textsuperscript{\(\star\)}: proof automation with SMT, tactics, and metaprograms
- Signature restriction for polymorphic algebraic effects
- Identifying overly restrictive matching patterns in SMT-based program verifiers (extended version)
- The dependently typed higher-order form for the TPTP world
- Reasoning about incompletely defined programs
- SMLtoCoq: automated generation of Coq specifications and proof obligations from SML programs with contracts
- The way we were: structural operational semantics research in perspective
- A mechanically verified garbage collector for OCaml
- Tableaux for automated reasoning in dependently-typed higher-order logic
- Isabelle/Solidity: A deep Embedding of Solidity in Isabelle/HOL
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)
