On the public citation graph

Mtac2: typed tactics for backward reasoning in Coq

https://doi.org/10.1145/3236773
0 signed · 47 inferred · view as graph

Inferred edges come from two machine sources: sweeps of open repository metadata (mostly SSRN and Zenodo), and a bulk OpenAlex citation snapshot. Every row below is labelled with the one it came from. Neither is a complete citation index — absence here is not evidence of absence.

Is this your work? Sign in with ORCID and put your name on the claims that are yours.
Claim with ORCID
Reference health. See whether every reference in this work resolves to a known work and none has been retracted — and get a dated CiteStamped badge you can embed.
See reference health

What this work says

Outgoing claims: the papers this work cites, builds on, or argues with.

inferredcites →https://doi.org/10.1007/978-3-319-08970-6_32openalex-snapshot
Universe Polymorphism in Coq
inferredcites →https://doi.org/10.1007/978-3-319-94821-8_17openalex-snapshot
Reification by Parametricity
inferredcites →https://doi.org/10.1007/978-3-319-94821-8_9openalex-snapshot
Tactics and Certificates in Meta Dedukti
inferredcites →https://doi.org/10.1007/978-3-540-71067-7_23openalex-snapshot
First-Class Type Classes
inferredcites →https://doi.org/10.1007/978-3-642-39634-2_8openalex-snapshot
Lightweight Proof by Reflection Using a Posteriori Simulation of Effectful Computation
inferredcites →https://doi.org/10.1007/978-3-662-49498-1_21openalex-snapshot
Extensible and Efficient Automation Through Reflective Tactics
inferredcites →https://doi.org/10.1016/0304-3975(92)90014-7openalex-snapshot
The revised report on the syntactic theories of sequential control and state
inferredcites →https://doi.org/10.1017/s0956796807006326openalex-snapshot
Applicative programming with effects
inferredcites →https://doi.org/10.1017/s0956796815000118openalex-snapshot
Mtac: A monad for typed tactic programming in Coq
inferredcites →https://doi.org/10.1017/s0956796818000151openalex-snapshot
Iris from the ground up: A modular foundation for higher-order concurrent separation logic
inferredcites →https://doi.org/10.1098/rsta.2014.0234openalex-snapshot
Tactics for mechanized reasoning: a commentary on Milner (1984) ‘The use of machines to assist in rigorous proof’
inferredcites →https://doi.org/10.1145/1328438.1328483openalex-snapshot
A type-theoretic foundation for programming with higher-order abstract syntax and first-class substitutions
inferredcites →https://doi.org/10.1145/1328897.1328483openalex-snapshot
A type-theoretic foundation for programming with higher-order abstract syntax and first-class substitutions
inferredcites →https://doi.org/10.1145/1352582.1352591openalex-snapshot
Contextual modal type theory
inferredcites →https://doi.org/10.1145/1863543.1863591openalex-snapshot
VeriML
inferredcites →https://doi.org/10.1145/2500365.2500579openalex-snapshot
Mtac
inferredcites →https://doi.org/10.1145/2951913.2951932openalex-snapshot
Elaborator reflection: extending Idris in Idris
inferredcites →https://doi.org/10.1145/3009837.3009855openalex-snapshot
Interactive proofs in higher-order concurrent separation logic
inferredcites →https://doi.org/10.1145/3093333.3009855openalex-snapshot
Interactive proofs in higher-order concurrent separation logic
inferredcites →https://doi.org/10.1145/3110278openalex-snapshot
A metaprogramming framework for formal verification
inferredcites →https://doi.org/10.1145/3133913openalex-snapshot
Robust and compositional verification of object capability patterns
inferredcites →https://doi.org/10.1145/3158152openalex-snapshot
A logical relation for monadic encapsulation of state: proving contextual equivalences in the presence of runST
inferredcites →https://doi.org/10.1145/3158154openalex-snapshot
RustBelt: securing the foundations of the Rust programming language
inferredcites →https://doi.org/10.1145/3236773openalex-snapshot
Mtac2: typed tactics for backward reasoning in Coq
inferredcites →https://doi.org/10.4230/lipics.ecoop.2017.17openalex-snapshot
Strong Logic for Weak Memory: Reasoning About Release-Acquire Consistency in Iris

What points at this work

Incoming claims: where this work appears in other papers’ reference lists and arguments.

inferred← backgroundhttps://doi.org/10.5281/zenodo.1307486zenodo-depositor-declared
Artifact For Mtac2: Typed Tactics For Backward Reasoning In Coq
inferred← citeshttps://doi.org/10.1007/978-3-030-17184-1_2openalex-snapshot
Meta-F $$^\star $$ : Proof Automation with SMT, Tactics, and Metaprograms
inferred← citeshttps://doi.org/10.1007/978-3-030-53518-6_17openalex-snapshot
The Tactician
inferred← citeshttps://doi.org/10.1007/978-3-030-79876-5_38openalex-snapshot
Harpoon: Mechanizing Metatheory Interactively
inferred← citeshttps://doi.org/10.1007/978-3-319-94821-8_9openalex-snapshot
Tactics and Certificates in Meta Dedukti
inferred← citeshttps://doi.org/10.1007/s10817-019-09540-0openalex-snapshot
The MetaCoq Project
inferred← citeshttps://doi.org/10.1016/j.jlamp.2021.100642openalex-snapshot
Verification of dynamic bisimulation theorems in Coq
inferred← citeshttps://doi.org/10.1109/rtss55097.2022.00026openalex-snapshot
From Intuition to Coq: A Case Study in Verified Response-Time Analysis 1 of FIFO Scheduling
inferred← citeshttps://doi.org/10.1145/3372297.3423352openalex-snapshot
HACLxN: Verified Generic SIMD Crypto (for all your favourite platforms)
inferred← citeshttps://doi.org/10.1145/3372885.3373812openalex-snapshot
FreeSpec: specifying, verifying, and executing impure computations in Coq
inferred← citeshttps://doi.org/10.1145/3437992.3439925openalex-snapshot
Lassie: HOL4 tactics by example
inferred← citeshttps://doi.org/10.1145/3437992.3439928openalex-snapshot
A novice-friendly induction tactic for lean
inferred← citeshttps://doi.org/10.1145/3607844openalex-snapshot
Modularity, Code Specialization, and Zero-Cost Abstractions for Program Verification
inferred← citeshttps://doi.org/10.1145/3704851openalex-snapshot
A Dependent Type Theory for Meta-programming with Intensional Analysis
inferred← citeshttps://doi.org/10.1561/2500000045openalex-snapshot
QED at Large: A Survey of Engineering of Formally Verified Software
inferred← citeshttps://doi.org/10.29007/wg1qopenalex-snapshot
Tactic Learning and Proving for the Coq Proof Assistant
inferred← citeshttps://doi.org/10.4204/eptcs.337.2openalex-snapshot
Touring the MetaCoq Project (Invited Paper)
inferred← citeshttps://doi.org/10.48550/arxiv.1803.06547openalex-snapshot
Meta-F*: Proof Automation with SMT, Tactics, and Metaprograms
inferred← citeshttps://doi.org/10.48550/arxiv.2107.07670openalex-snapshot
Touring the MetaCoq Project (Invited Paper)
inferred← citeshttps://doi.org/10.70675/0a3f5dbaza45az464dz8686z8c853cf21497openalex-snapshot
Prétraitement compositionnel en Coq
inferred← citeshttps://doi.org/10.70675/7d8a27b4zebf6z43c3z9577zeaa9e6c64d97openalex-snapshot
Challenges in the collaborative evolution of a proof language and its ecosystem
showing the first 21 of 22 · page through all 22
Editorial review for independent work. ICSAC — the Institute for Complexity Science and Advanced Computing — runs a structured editorial panel for researchers publishing outside journals, and publishes on CiteStamp rails. Submission is free and goes through ORCID: icsacinstitute.org/submit.