Proof reflection in Coq
type: Item
instance of: scholarly article
title: Proof reflection in Coq
zbMATH Open document ID: 1012.03018
DOI: 10.1023/A:1021923116629
author: Dimitri Hendriks
published in: Journal of Automated Reasoning
publication date: 2003-04-27T00:00:00Z
Mathematics Subject Classification ID: 03B35
Mathematics Subject Classification ID: 68T15
zbMATH DE Number: 1901557
zbMATH Keywords: Coq
zbMATH Keywords: formalization of logical systems
zbMATH Keywords: reflection
zbMATH Keywords: natural deduction
zbMATH Keywords: first-order logic
zbMATH Keywords: reduction relation on proof terms
describes a project that uses: Coq
MaRDI profile type: MaRDI publication profile
full work available at URL: a:1021923116629
OpenAlex ID: W1611906969
Recommended article: Proof by computation in the Coq system
Recommended article: Proof theory of reflection
Recommended article: Q2766536
Recommended article: Q3138833
Recommended article: Q3075246
Recommended article: From Proposition to Program
Recommended article: Practical Proof Search for Coq by Type Inhabitation
Recommended article: A Proof System for MSVL Programs in Coq
Recommended article: A formal proof in Coq of Lasalle's invariance principle
Recommended article: Ornaments for Proof Reuse in Coq
description: scientific article; zbMATH DE number 1901557