A reflection−based proof tactic for lattices in Coq

A reflection−based proof tactic for lattices in Coq

Taispeáin leaganacha eile (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...

Cur síos iomlán

Sonraí bibleagrafaíochta
Príomhchruthaitheoirí:	James, D, Hinze, R
Rannpháirtithe:	Horváth, Z
Formáid:	LEABHAR
Foilsithe / Cruthaithe:	2009

Míreanna comhchosúla

A Reflection−based Proof Tactic for Lattices in Coq
de réir: James, D, et al.
Foilsithe / Cruthaithe: (2009)

A reflection−based proof tactic for lattices in Coq
de réir: James, D, et al.
Foilsithe / Cruthaithe: (2010)

CoqIOA : a formalization of IO automata in the Coq proof assistant
de réir: Athalye, Anish (Anish R.)
Foilsithe / Cruthaithe: (2017)

A Machine Proof System of Point Geometry Based on Coq
de réir: Siran Lei, et al.
Foilsithe / Cruthaithe: (2023-06-01)

Formal Proof of a Machine Closed Theorem in Coq
de réir: Hai Wan, et al.
Foilsithe / Cruthaithe: (2014-01-01)

An introduction to small scale reflection in Coq
de réir: Georges Gonthier, et al.
Foilsithe / Cruthaithe: (2010-01-01)

Sets in Coq, Coq in Sets
de réir: Bruno Barras
Foilsithe / Cruthaithe: (2010-01-01)

Learning how to Prove: From the Coq Proof Assistant to Textbook Style
de réir: Sebastian Böhne, et al.
Foilsithe / Cruthaithe: (2018-03-01)

Certified programming with dependent types : a pragmatic introduction to the Coq proof assistant /
de réir: Chlipala, Adam, 1981-
Foilsithe / Cruthaithe: (2013)

A Comprehensive Formalization of Propositional Logic in Coq: Deduction Systems, Meta-Theorems, and Automation Tactics
de réir: Dakai Guo, et al.
Foilsithe / Cruthaithe: (2023-05-01)

Towards a Scalable Proof Engine: A Performant Prototype Rewriting Primitive for Coq
de réir: Gross, Jason, et al.
Foilsithe / Cruthaithe: (2024)

Company-Coq: Taking Proof General one step closer to a real IDE
de réir: Pit-Claudel, Clement F., et al.
Foilsithe / Cruthaithe: (2016)

Company-Coq: Taking Proof General one step closer to a real IDE
de réir: Pit-Claudel, Clément, et al.
Foilsithe / Cruthaithe: (2021)

Le coq médiéval
de réir: Michel Pastoureau
Foilsithe / Cruthaithe: (2017-12-01)

Generic Programs and Proofs
de réir: Hinze, R
Foilsithe / Cruthaithe: (2000)

Characterization of <i>Arabidopsis thaliana</i> Coq9 in the CoQ Biosynthetic Pathway
de réir: Mei Hu, et al.
Foilsithe / Cruthaithe: (2023-06-01)

Deciding Kleene Algebras in Coq
de réir: Thomas Braibant, et al.
Foilsithe / Cruthaithe: (2012-03-01)

CoQ10 and Aging
de réir: Isabella Peixoto de Barcelos, et al.
Foilsithe / Cruthaithe: (2019-05-01)

PIDE for Asynchronous Interaction with Coq
de réir: Carst Tankink
Foilsithe / Cruthaithe: (2014-10-01)

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

Automatic Generation of Proof Tactics for Finite-Valued Logics
de réir: João Marcos
Foilsithe / Cruthaithe: (2010-03-01)

Scans and Convolutions—A Calculational Proof of Moessner's Theorem
de réir: Hinze, R
Foilsithe / Cruthaithe: (2009)

Encephalopathy, kidney failure and retinopathy. CoQ10 deficiency due to COQ8B mutation
de réir: Victor Adam Lancet, et al.
Foilsithe / Cruthaithe: (2021-06-01)

Scans and Convolutions-A Calculational Proof of Moessner's Theorem
de réir: Hinze, R
Foilsithe / Cruthaithe: (2011)

Scans and Convolutions—A Calculational Proof of Moessner's Theorem
de réir: Hinze, R
Foilsithe / Cruthaithe: (2011)

Computable analysis and notions of continuity in Coq
de réir: Florian Steinberg, et al.
Foilsithe / Cruthaithe: (2021-05-01)

Manganese-driven CoQ deficiency
de réir: Jutta Diessl, et al.
Foilsithe / Cruthaithe: (2022-10-01)

Formalization of Quantum Protocols using Coq
de réir: Jaap Boender, et al.
Foilsithe / Cruthaithe: (2015-11-01)

LF+ in Coq for "fast and loose" reasoning
de réir: Fabio Alessi, et al.
Foilsithe / Cruthaithe: (2019-12-01)

Enseñando métodos formales con Coq
de réir: Carlos Daniel Luna
Foilsithe / Cruthaithe: (2006-12-01)

Enseñando métodos formales con Coq
de réir: Luna, Carlos Daniel
Foilsithe / Cruthaithe: (2006-01-01)

Correct-by-construction finite field arithmetic in Coq
de réir: Philipoom, Jade (Jade D.)
Foilsithe / Cruthaithe: (2018)

Zero-knowledge proof systems for lattice-based cryptography
de réir: Nguyen, Ta Toan Khoa
Foilsithe / Cruthaithe: (2014)

Novel recessive mutations in COQ4 cause severe infantile cardiomyopathy and encephalopathy associated with CoQ10 deficiency
de réir: Neal Sondheimer, et al.
Foilsithe / Cruthaithe: (2017-09-01)

A systematic derivation of the STG machine verified in Coq
de réir: Pirog, M, et al.
Foilsithe / Cruthaithe: (2010)

Human COQ10A and COQ10B are distinct lipid-binding START domain proteins required for coenzyme Q function[S]
de réir: Hui S. Tsui, et al.
Foilsithe / Cruthaithe: (2019-07-01)

Proof of Tacticity of Stereoregular ROMP Polymers through Post Polymerization Modification
de réir: Hyvl, Jakub, et al.
Foilsithe / Cruthaithe: (2017)

Formalising and Verifying Reference Attribute Grammars in Coq.
de réir: Schäfer, M, et al.
Foilsithe / Cruthaithe: (2009)

Formalising and Verifying Reference Attribute Grammars in Coq
de réir: Schäfer, M, et al.
Foilsithe / Cruthaithe: (2009)

The impact of COQ on the profitability and competitiveness of companies in Singapore.
de réir: Chan, Wai Yee., et al.
Foilsithe / Cruthaithe: (2013)