Cited in
(61)- Automated type-based analysis of injective agreement in the presence of compromised principals
- System-level non-interference of constant-time cryptography. II: Verified static analysis and stealth memory
- I got plenty o' nuttin'
- Program synthesis for interactive-security systems
- Unified syntax with iso-types
- The essence of ornaments
- Cryptographic Verification by Typing for a Sample Protocol Implementation
- Dijkstra monads for free
- Proof-carrying code in a session-typed process calculus
- COSTA
- CASPA_
- Probabilistic functions and cryptographic oracles in higher order logic
- AURA
- Flow Caml
- OFMC
- Cayenne
- EasyCrypt
- Irdis
- ASPIER
- Cryptyc
- Aglet
- pGCL
- TS#
- AIOCJ
- Ur/Web
- Idris
- JFlow
- Scribble
- SAVARA
- Lolliproc
- SPY
- EROS
- Fable
- Laminar
- Merlin
- Moat
- Privtrans
- VC3
- Information flow analysis for valued-indexed data security compartments
- CoSP
- apims
- JSLINQ
- TaintDroid
- CryptHOL: game-based proofs in higher-order logic
- Bedrock
- SeLINQ
- Links
- Zoo Probabilistic Systems
- GREEND
- CacheAudit
- JSFlow
- HACL*
- Game_Based_Crypto
- MFMC_Countable
- Probabilistic_While
- A gentle introduction to multiparty asynchronous session types
- Combining behavioural types with security analysis
- A delta for hybrid type checking
- Implicit computational complexity of subrecursive definitions and applications to cryptographic proofs
- Formal methods for web security
- A Classical Realizability Model for a Semantical Value Restriction
This page was built for software: F*
