An introduction to small scale reflection in Coq
From MaRDI portal
Recommendations
- An Essence of SSReflect
- Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
- An introduction to programming and proving with dependent types in Coq
- Canonical structures for the working Coq user
- A Short Presentation of Coq
Cited in
(42)- Proof-producing reflection for HOL. With an application to model polymorphism
- Designing and proving correct a convex hull algorithm with hypermaps in Coq
- A Decision Procedure for Regular Expression Equivalence in Type Theory
- From Sets to Bits in Coq
- Coquet: a Coq library for verifying hardware
- scientific article; zbMATH DE number 1863396 (Why is no real title available?)
- Proof-relevant Horn clauses for dependent type inference and term synthesis
- Proof reflection in Coq
- An intuitionistic proof of a discrete form of the Jordan curve theorem formalized in Coq with combinatorial hypermaps
- A certified reduction strategy for homological image processing
- Finite Groups Representation Theory with Coq
- Incidence simplicial matrices formalized in Coq/SSReflect
- Eisbach: a proof method language for Isabelle
- Implementation of Bourbaki's \textit{Elements of mathematics} in Coq. II: From natural numbers to real numbers
- Computational Complexity Via Finite Types
- Certifying assembly with formal security proofs: the case of BBS
- Formalising Mathematics in Simple Type Theory
- Theorem of three circles in Coq
- A formalization of multi-tape Turing machines
- Universal algebra in UniMath
- Proof mining with dependent types
- Partiality, state and dependent types
- Some Wellfounded Trees in UniMath
- Point-free, set-free concrete linear algebra
- Recycling proof patterns in Coq: case studies
- Packaging Mathematical Structures
- From LCF to Isabelle/HOL
- Formalization of the Domination Chain with Weighted Parameters (Short Paper)
- Formalization techniques for asymptotic reasoning in classical analysis
- Trace-Based Coinductive Operational Semantics for While
- A practical formalization of monadic equational reasoning in dependent-type theory
- Formally verified certificate checkers for hardest-to-round computation
- Foundations of dependent interoperability
- On the maximum weighted irredundant set problem
- Hammer for Coq: automation for dependent type theory
- \textsc{CoqCryptoLine}: a verified model checker with certified results
- Certified verification for algebraic abstraction
- Foundational property-based testing
- Towards automatic transformations of Coq proof scripts
- scientific article; zbMATH DE number 7649962 (Why is no real title available?)
- A Short Presentation of Coq
- Canonical Big Operators
This page was built for publication: An introduction to small scale reflection in Coq
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3075246)
