Combining proofs and programs in a dependently typed language

Article Details
Title:	Combining proofs and programs in a dependently typed language
Article URLs:	https://doi.org/10.1145/2535838.2535883
Alternative Article URLs:
Authors:	Chris Casinghino	University of Pennsylvania
	Vilhelm Sjöberg	University of Pennsylvania
	Stephanie Weirich	University of Pennsylvania
Sharing:	Unknown
Verification:	Authors have not verified information
Artifact Evaluation Badge:	none
Artifact URLs:	http://www.cis.upenn.edu/~ccasin/papers/combining-coq.tgz https://github.com/sweirich/trellys/tree/zombie-trellys-POPL14
Artifact Correspondence Email Addresses:
NSF Award Numbers:	0910500, 1116620
DBLP Key:	conf/popl/CasinghinoSW14
Author Comments:

ACM Principles of Programming Languages, POPL 2014