A reflection−based proof tactic for lattices in Coq

A reflection−based proof tactic for lattices in Coq

Show other versions (2)

Bibliographic Details
Main Authors:	James, D, Hinze, R
Format:	Conference item
Published:	Intellect 2010

Similar Items

A reflection−based proof tactic for lattices in Coq
by: James, D, et al.
Published: (2009)

A Reflection−based Proof Tactic for Lattices in Coq
by: James, D, et al.
Published: (2009)

CoqIOA : a formalization of IO automata in the Coq proof assistant
by: Athalye, Anish (Anish R.)
Published: (2017)

A Machine Proof System of Point Geometry Based on Coq
by: Siran Lei, et al.
Published: (2023-06-01)

An introduction to small scale reflection in Coq
by: Georges Gonthier, et al.
Published: (2010-01-01)

Sets in Coq, Coq in Sets
by: Bruno Barras
Published: (2010-01-01)

Learning how to Prove: From the Coq Proof Assistant to Textbook Style
by: Sebastian Böhne, et al.
Published: (2018-03-01)

Certified programming with dependent types : a pragmatic introduction to the Coq proof assistant /
by: Chlipala, Adam, 1981-
Published: (2013)

A Comprehensive Formalization of Propositional Logic in Coq: Deduction Systems, Meta-Theorems, and Automation Tactics
by: Dakai Guo, et al.
Published: (2023-05-01)

Mechanization of pomset languages in the Coq proof assistant for the specification of weak memory models
by: Evgenii A. Moiseenko, et al.
Published: (2022-06-01)

Towards a Scalable Proof Engine: A Performant Prototype Rewriting Primitive for Coq
by: Gross, Jason, et al.
Published: (2024)

Company-Coq: Taking Proof General one step closer to a real IDE
by: Pit-Claudel, Clément, et al.
Published: (2021)

Company-Coq: Taking Proof General one step closer to a real IDE
by: Pit-Claudel, Clement F., et al.
Published: (2016)

Le coq médiéval
by: Michel Pastoureau
Published: (2017-12-01)

Generic Programs and Proofs
by: Hinze, R
Published: (2000)

Characterization of <i>Arabidopsis thaliana</i> Coq9 in the CoQ Biosynthetic Pathway
by: Mei Hu, et al.
Published: (2023-06-01)

Automatic Generation of Proof Tactics for Finite-Valued Logics
by: João Marcos
Published: (2010-03-01)

Deciding Kleene Algebras in Coq
by: Thomas Braibant, et al.
Published: (2012-03-01)

CoQ10 and Aging
by: Isabella Peixoto de Barcelos, et al.
Published: (2019-05-01)

PIDE for Asynchronous Interaction with Coq
by: Carst Tankink
Published: (2014-10-01)

Human COQ9 Rescues a coq9 Yeast Mutant by Enhancing Coenzyme Q Biosynthesis from 4-Hydroxybenzoic Acid and Stabilizing the CoQ-Synthome
by: Cuiwen H. He, et al.
Published: (2017-07-01)

Encephalopathy, kidney failure and retinopathy. CoQ10 deficiency due to COQ8B mutation
by: Victor Adam Lancet, et al.
Published: (2021-06-01)

Scans and Convolutions—A Calculational Proof of Moessner's Theorem
by: Hinze, R
Published: (2011)

Scans and Convolutions-A Calculational Proof of Moessner's Theorem
by: Hinze, R
Published: (2011)

Scans and Convolutions—A Calculational Proof of Moessner's Theorem
by: Hinze, R
Published: (2009)

Zero-knowledge proof systems for lattice-based cryptography
by: Nguyen, Ta Toan Khoa
Published: (2014)

Computable analysis and notions of continuity in Coq
by: Florian Steinberg, et al.
Published: (2021-05-01)

Manganese-driven CoQ deficiency
by: Jutta Diessl, et al.
Published: (2022-10-01)

Formalization of Quantum Protocols using Coq
by: Jaap Boender, et al.
Published: (2015-11-01)

LF+ in Coq for "fast and loose" reasoning
by: Fabio Alessi, et al.
Published: (2019-12-01)

Enseñando métodos formales con Coq
by: Carlos Daniel Luna
Published: (2006-12-01)

Correct-by-construction finite field arithmetic in Coq
by: Philipoom, Jade (Jade D.)
Published: (2018)

Novel recessive mutations in COQ4 cause severe infantile cardiomyopathy and encephalopathy associated with CoQ10 deficiency
by: Neal Sondheimer, et al.
Published: (2017-09-01)

A systematic derivation of the STG machine verified in Coq
by: Pirog, M, et al.
Published: (2010)

Human COQ10A and COQ10B are distinct lipid-binding START domain proteins required for coenzyme Q function[S]
by: Hui S. Tsui, et al.
Published: (2019-07-01)

Proof of Tacticity of Stereoregular ROMP Polymers through Post Polymerization Modification
by: Hyvl, Jakub, et al.
Published: (2017)

Formalising and Verifying Reference Attribute Grammars in Coq.
by: Schäfer, M, et al.
Published: (2009)

Formalising and Verifying Reference Attribute Grammars in Coq
by: Schäfer, M, et al.
Published: (2009)

Hilbert's Tenth Problem in Coq (Extended Version)
by: Dominique Larchey-Wendling, et al.
Published: (2022-03-01)

Coinductive Natural Semantics for Compiler Verification in Coq
by: Angel Zúñiga, et al.
Published: (2020-09-01)