Dependent types and multi-monadic effects in F*

No abstract is available for this paper.

• Publication year

  2016

• Venue

  ACM-SIGACT Symposium on Principles of Programming Languages

• Publication date

  2016-01-11

• Fields of study

  Computer Science

• Identifiers
  DOI 10.1145/2837614.2837655
• External record

  Open on Semantic Scholar

• Source metadata

  Semantic Scholar

• No claims are published for this paper.

• No concepts are published for this paper.

• Autosubst: Reasoning with de Bruijn Terms and Parallel Substitutions

  2015cited by this paper
• Combining proofs and programs in a dependently typed language

  2014influential reference
• Refinement types for Haskell

  2014influential reference
• Verifying higher-order programs with the dijkstra monad

  2013influential reference
• Implementing TLS with Verified Cryptographic Security

  2013influential reference
• Why3 - Where Programs Meet Provers

  2013cited by this paper
• Programming and reasoning with algebraic effects and dependent types

  2013influential reference
• Equational reasoning about programs with general recursion and call-by-value semantics

  2012cited by this paper
• Strongly Typed Term Representations in Coq

  2012cited by this paper
• Secure distributed programming with value-dependent types

  2011influential reference
• Termination of Isabelle Functions via Termination of Rewriting

  2011cited by this paper
• Dafny: An Automatic Program Verifier for Functional Correctness

  2010influential reference
• Modular verification of security protocol code by typing

  2010influential reference
• Effective interactive proofs for higher-order imperative programs

  2009cited by this paper
• Extraction in Coq: An Overview

  2008influential reference
• Liquid types

  2008influential reference
• The Transport Layer Security (TLS) Protocol Version 1.3

  2008cited by this paper
• Hoare type theory, polymorphism and separation1

  2008influential reference
• Type-based termination: a polymorphic lambda-calculus with sized higher-order types

  2006cited by this paper
• Subset Coercions in Coq

  2006cited by this paper
• Combining programming with theorem proving

  2005influential reference
• Type-based termination of recursive denitions

  2004cited by this paper
• Formalized Metatheory with Terms Represented by an Indexed Family of Types

  2004cited by this paper
• Authenticated-encryption with associated-data

  2002cited by this paper
• Simple General Recursion in Type Theory

  2001cited by this paper
• Monadic Presentations of Lambda Terms Using Generalized Inductive Types

  1999cited by this paper
• Cayenne—a language with dependent types

  1998influential reference
• Subtypes for Specifications: Predicate Subtyping in PVS

  1998cited by this paper
• Region-based Memory Management

  1997cited by this paper
• Reasoning about Aliasing

  1996cited by this paper
• Refinement types for ML

  1991cited by this paper
• Computational lambda-calculus and monads

  1989cited by this paper
• Implementing mathematics with the Nuprl proof development system

  1986cited by this paper
• Report on the programming language Euclid

  1977cited by this paper
• Guarded commands, nondeterminacy and formal derivation of programs

  1975cited by this paper
• Towards a Mathematical Science of Computation

  1962cited by this paper
• Under Consideration for Publication in J. Functional Programming Mtac: a Monad for Typed Tactic Programming in Coq

  year unknowncited by this paper
• Íòòòö Óò××××öøøóò Óö Ôùùðð Blockinøøóò Ò Ååøøº Ëøöù Blockinøº Ò Óñôº Ë Blockin Blockin Blockinò Ìýô¹¹¹××× Øøöññòòøøóò Óó Öö Blockinùö××ú ¬òòøøóò×

  year unknowncited by this paper
• Under Consideration for Publication in J. Functional Programming Parameterised Notions of Computation

  year unknowncited by this paper

• Foundational Multi-Modal Program Verifiers

  2026cites this paper
• Encode the Cake and Eat It Too: Controlling Computation in Type Theory, Locally

  2026cites this paper
• Building Blocks for Step-Indexed Program Logics

  2026cites this paper
• The Verification Theater: When Formal Methods Create False Assurance in Cryptographic Libraries

  2026cites this paper
• Misquoted No More: Securely Extracting F* Programs with IO

  2026cites this paper
• Bounded First-Class Universe Levels in Dependent Type Theory

  2025cites this paper
• PulseCore: An Impredicative Concurrent Separation Logic for Dependently Typed Programs

  2025cites this paper
• Atmosphere: Practical Verified Kernels with Rust and Verus

  2025cites this paper
• The Dependently Typed Higher-Order Form for the TPTP World

  2025cites this paper
• UAV Resilience Against Stealthy Attacks

  2025cites this paper
• Verifying Properties of Index Arrays in a Purely-Functional Data-Parallel Language

  2025cites this paper
• Gpass: A Goal-Adaptive Neural Theorem Prover Based on Coq for Automated Formal Verification

  2025cites this paper
• Probabilistic Refinement Session Types

  2025cites this paper
• A Mechanically Verified Garbage Collector for OCaml

  2025cites this paper
• Efficient Formal Verification of Quantum Error Correcting Programs

  2025cites this paper
• Inferring multiple helper Dafny assertions with LLMs

  2025cites this paper
• ProofWright: Towards Agentic Formal Verification of CUDA

  2025cites this paper
• Who Verifies the Verifiers? Lessons Learned From Formally Verified Line-Point Zero-Knowledge

  2025cites this paper
• Enforcing MAVLink Safety & Security Properties Via Refined Multiparty Session Types

  2025cites this paper
• Ghost in the Android Shell: Pragmatic Test-oracle Specification of a Production Hypervisor

  2025cites this paper
• Smooth, Integrated Proofs of Cryptographic Constant Time for Nondeterministic Programs and Compilers

  2025cites this paper
• Neurosymbolic Modular Refinement Type Inference

  2025cites this paper
• AdapTT: Functoriality for Dependent Type Casts

  2025cites this paper
• Secure Parsing and Serializing with Separation Logic Applied to CBOR, CDDL, and COSE

  2025cites this paper
• Raven: An SMT-Based Concurrency Verifier

  2025cites this paper
• TreeKEM: A Modular Machine-Checked Symbolic Security Analysis of Group Key Agreement in Messaging Layer Security

  2025cites this paper
• Formal Security and Functional Verification of Cryptographic Protocol Implementations in Rust

  2025influential citation
• On the Impact of Formal Verification on Software Development

  2025cites this paper
• Can Large Language Models Verify System Software? A Case Study Using FSCQ as a Benchmark

  2025cites this paper
• Dynamic Verification of OCaml Software with Gospel and Ortac/QCheck-STM

  2025cites this paper
• Modeling the composition of analysis components and automatic constraint checking for semantic soundness

  2025cites this paper
• Who Verifies the Verifiers?: Lessons Learned From Formally Verified Line-Point Zero-Knowledge

  2025cites this paper
• Listening to the Firehose: Sonifying Z3’s Behavior

  2025cites this paper
• Secure Satellite Software-Defined Payloads With High-Assurance Post-Quantum Cryptography

  2025cites this paper
• Internalizing Extensions in Lattices of Type Theories

  2025cites this paper
• Toward Practical Deductive Verification: Insights from a Qualitative Survey in Industry and Academia

  2025cites this paper
• Lean4Less: Eliminating Definitional Equalities from Lean via an Extensional-to-Intensional Translation

  2025cites this paper
• MiniF2F-Dafny: LLM-Guided Mathematical Theorem Proving via Auto-Active Verification

  2025cites this paper
• Operationalizing CaMeL: Strengthening LLM Defenses for Enterprise Deployment

  2025cites this paper
• Verified VCG and Verified Compiler for Dafny

  2025cites this paper
• Quantified Underapproximation via Labeled Bunches

  2025cites this paper
• Compiling by Proving: Language-Agnostic Automatic Optimization from Formal Semantics

  2025cites this paper
• BLACKOUT: Data-Oblivious Computation with Blinded Capabilities

  2025cites this paper
• Accelerating Automated Program Verifiers by Automatic Proof Localization

  2025cites this paper
• Automatically Verifying Replication-Aware Linearizability

  2025cites this paper
• Memory-Safety Verification of Open Programs with Angelic Assumptions

  2025cites this paper
• The Squirrel Prover and its Logic

  2024cites this paper
• Context Pruning for More Robust SMT-based Program Verification

  2024cites this paper
• AutoVerus: Automated Proof Generation for Rust Code

  2024cites this paper
• Multris: Functional Verification of Multiparty Message Passing in Separation Logic

  2024cites this paper
• Free Facts: An Alternative to Inefficient Axioms in Dafny

  2024cites this paper
• Towards Neural Synthesis for SMT-Assisted Proof-Oriented Programming

  2024cites this paper
• QEDCartographer: Automating Formal Verification Using Reward-Free Reinforcement Learning

  2024cites this paper
• Formalizing, Mechanizing, and Verifying Class-Based Refinement Types

  2024cites this paper
• StarMalloc: Verifying a Modern, Hardened Memory Allocator

  2024cites this paper
• A Framework for Debugging Automated Program Verification Proofs via Proof Actions

  2024cites this paper
• InferType: A Compiler Toolkit for Implementing Efficient Constraint-Based Type Inference (Artifact)

  2024cites this paper
• Ethereum smart contract security: Design, risks and protection approaches

  2024cites this paper
• miniCodeProps: a Minimal Benchmark for Proving Code Properties

  2024cites this paper
• Dependent Ghosts Have a Reflection for Free

  2024cites this paper
• Modular Verification of Secure and Leakage-Free Systems: From Application Specification to Circuit-Level Implementation

  2024cites this paper
• Synchronous Programming with Refinement Types

  2024cites this paper
• Tableaux for Automated Reasoning in Dependently-Typed Higher-Order Logic

  2024cites this paper
• hax: Verifying Security-Critical Rust Software using Multiple Provers

  2024cites this paper
• Laurel: Unblocking Automated Verification with Large Language Models

  2024cites this paper
• StarMalloc: A Formally Verified, Concurrent, Performant, and Security-Oriented Memory Allocator

  2024cites this paper
• Bending microarchitectural weird machines towards practicality

  2024cites this paper
• Sound Borrow-Checking for Rust via Symbolic Semantics

  2024cites this paper
• SECOMP: Formally Secure Compilation of Compartmentalized C Programs

  2024cites this paper
• Data-Oblivious ML Accelerators Using Hardware Security Extensions

  2024cites this paper
• KestRel: Relational Verification using E-Graphs for Program Alignment

  2024cites this paper
• DY Fuzzing: Formal Dolev-Yao Models Meet Cryptographic Protocol Fuzz Testing

  2024cites this paper
• AlphaVerus: Bootstrapping Formally Verified Code Generation through Self-Improving Translation and Treefinement

  2024cites this paper
• Automatic generation of security protocols attacks specifications and implementations

  2024cites this paper
• Scylla: Translating an Applicative Subset of C to Safe Rust

  2024cites this paper
• Veld: Verified Linux Drivers

  2024cites this paper
• OBRA: Oracle-Based, Relational, Algorithmic Type Verification

  2024cites this paper
• MimIR: An Extensible and Type-Safe Intermediate Representation for the DSL Age

  2024cites this paper
• Formal Foundations for Translational Separation Logic Verifiers

  2024cites this paper
• Algebraic Effects Meet Hoare Logic in Cubical Agda

  2024cites this paper
• Automated Proof Generation for Rust Code via Self-Evolution

  2024cites this paper
• Verus: A Practical Foundation for Systems Verification

  2024influential citation
• Towards SMT Solver Stability via Input Normalization

  2024cites this paper
• Towards Provable Security in Industrial Control Systems Via Dynamic Protocol Attestation

  2024cites this paper
• Compiling High-Level Neural Network Specifications into VNN-LIB Queries

  2024cites this paper
• Extensionality of Ghost Dependent Types for Free

  2023cites this paper
• Comparse: Provably Secure Formats for Cryptographic Protocols

  2023cites this paper
• Stratified Type Theory

  2023cites this paper
• Layered Symbolic Security Analysis in DY$^\star$

  2023cites this paper
• $\mathcal{P}\text{ARseL}$: Towards a Verified Root-of-Trust Over seL4

  2023cites this paper
• Higher-Order Property-Directed Reachability

  2023cites this paper
• Type-directed Program Transformation for Constant-Time Enforcement

  2023cites this paper
• From Dragondoom to Dragonstar: Side-channel Attacks and Formally Verified Implementation of WPA3 Dragonfly Handshake

  2023cites this paper
• Securing Verified IO Programs Against Unverified Code in F*

  2023cites this paper
• Answer Refinement Modification: Refinement Type System for Algebraic Effects and Handlers

  2023cites this paper
• An Opcode-Based Vulnerability Detection of Smart Contracts

  2023cites this paper
• Interaction Tree Specifications: A Framework for 15 Specifying Recursive, Effectful Computations that 16 Supports Auto-active Verification

  2023cites this paper
• Securely Compiling F ★ Programs With IO and Then Linking Them Against Weakly-Typed Interfaces

  2023cites this paper
• Interaction Tree Specifications: A Framework for Specifying Recursive, Effectful Computations That Supports Auto-Active Verification (Artifact)

  2023cites this paper
• 2022 ACTIVITY REPORT Project-Team GALLINETTE

  2023cites this paper