Extraction of redundancy-free programs from constructive natural deduction proofs
type: Item
instance of: scholarly article
title: Extraction of redundancy-free programs from constructive natural deduction proofs
zbMATH Open document ID: 0731.68079
DOI: 10.1016/S0747-7171(08)80139-3
author: Yukihide Takayama
published in: Journal of Symbolic Computation
publication date: 1991-01-01T00:00:00Z
Mathematics Subject Classification ID: 68Q60
zbMATH DE Number: 4209628
zbMATH Keywords: automated programming
zbMATH Keywords: program verification
zbMATH Keywords: redundancy-free codes
zbMATH Keywords: proof trees
zbMATH Keywords: realizability interpretation
zbMATH Keywords: constructive logic
describes a project that uses: Nuprl
MaRDI profile type: Publication
cites work: Q3679172
cites work: The calculus of constructions
cites work: Q3880322
cites work: Q3922646
cites work: Q5559220
cites work: Q5183475
description: scientific article; zbMATH DE number 4209628