A reflection−based proof tactic for lattices in Coq

A reflection−based proof tactic for lattices in Coq

Show other versions (2)

This paper presents a new proof tactic that decides equalities and inequalities between terms over lattices. It uses a decision procedure that is a variation on Whitman’s algorithm and is implemented using a technique known as proof by reflection. We will paint the essence of the approach in broad...

Fuld beskrivelse

Bibliografiske detaljer
Main Authors:	James, D, Hinze, R
Andre forfattere:	Horváth, Z
Format:	Bog
Udgivet:	2009

Lignende værker

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

A reflection−based proof tactic for lattices in Coq
af: James, D, et al.
Udgivet: (2010)

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

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

Formal Proof of a Machine Closed Theorem in Coq
af: Hai Wan, et al.
Udgivet: (2014-01-01)

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

Sets in Coq, Coq in Sets
af: Bruno Barras
Udgivet: (2010-01-01)

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

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

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

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

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

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

Le coq médiéval
af: Michel Pastoureau
Udgivet: (2017-12-01)

Generic Programs and Proofs
af: Hinze, R
Udgivet: (2000)

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

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

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

PIDE for Asynchronous Interaction with Coq
af: Carst Tankink
Udgivet: (2014-10-01)

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

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

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

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

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

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

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

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

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

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

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

Enseñando métodos formales con Coq
af: Luna, Carlos Daniel
Udgivet: (2006-01-01)

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

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

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

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

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

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

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

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

The impact of COQ on the profitability and competitiveness of companies in Singapore.
af: Chan, Wai Yee., et al.
Udgivet: (2013)