Paper Info
Title
A Comparison of HOL and ALF Formalizations of a Categorical Coherence Theorem
Abstract
. We compare formalizations of an example from elementarycategory theory in the systems HOL (an implementation of Church'sclassical simple type theory) and ALF (an implementation of MartinLof's intuitionistic type theory). The example is a proof of coherence formonoidal categories which was extracted from a proof of normalizationfor monoids. It makes essential use of the identification of proofs andprograms which is fundamental to intuitionistic type theory. This aspectis naturally...
Year
DOI
Venue
1996
10.1007/BFb0105394
TPHOLs
Keywords
Field
DocType
alf formalizations,categorical coherence theorem,type theory
HOL,Monoidal category,Intuitionistic type theory,Computer science,Algorithm,Type theory,Mathematical proof,Monoid,Category theory,Coherence theorem
Conference
ISBN
Citations 
PageRank 
3-540-61587-3
2
0.81
References 
Authors
6
3
Name
Order
Citations
PageRank
Sten Agerholm19511.40
Ilya Beylin2203.52
Peter Dybjer354076.99