projects / coq-hetmet.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 70939a4) | patch
proofs that Types/Judgments form an enrichment
authorAdam Megacz <megacz@cs.berkeley.edu>
Tue, 22 Mar 2011 01:26:58 +0000 (18:26 -0700)
committerAdam Megacz <megacz@cs.berkeley.edu>
Tue, 22 Mar 2011 01:26:58 +0000 (18:26 -0700)
commit85e4f0fd6b0673c1cc763eeb2585b7dc3d388455
treebda5a9d595c8c7099f43a377f84b6a4adfcb162dtree | snapshot
parent70939a4eb9560ceeea3e9cf176ac5a36f9201ac4commit | diff
proofs that Types/Judgments form an enrichment
src/HaskProofCategory.v diff | blob | history
src/HaskStrongCategory.v diff | blob | history
src/NaturalDeduction.v diff | blob | history
src/NaturalDeductionCategory.v diff | blob | history
src/ProgrammingLanguage.v [new file with mode: 0644] blob
src/ReificationsEquivalentToGeneralizedArrows.v diff | blob | history
Coq proofs and code accompanying the HetMet extensions for GHC