SURVEY:SUMMARY:BUILD_DIFFICULTY[not_applicable, reasonable_effort, code_problematic or string] reasonable_effort
SURVEY:SUMMARY:CLASSIFICATION[practical,theoretical,hardware] practical
SURVEY:SUMMARY:CORRECT_CODE_LOCATION[string] 
SURVEY:SUMMARY:PUBLISHED_CODE[not_applicable, yes, no] yes
SURVEY:SUMMARY:SAME_VERSION[not_applicable, yes, no_but_available, no_and_not_available] yes
SURVEY:SUMMARY:STUDY_FOUND_CORRECT_CODE[not_applicable, yes, no] yes
SURVEY:AUTHOR1:BUILD_COMMENT[string] 
SURVEY:AUTHOR1:BUILD_DIFFICULTY[not_applicable, reasonable_effort, code_problematic or string] reasonable_effort
SURVEY:AUTHOR1:BUILD_DIFFICULTY_COMMENT[string] Coq proofs (such as our downloadable artifact) may pose a problem after a while, because the Coq system tends to introduce changes breaking backward compatibility; downloaders may therefore have to use a version of Coq which is not the very newest one. Our Coq proof is of course affected by this problem, just like all other Coq proofs.
SURVEY:AUTHOR1:CLASSIFICATION[practical,theoretical,hardware] practical
SURVEY:AUTHOR1:CLASSIFICATION_COMMENT[string] I am using the same classification as yours, according to the email message that took me here.  However, it seems likely that this classification as "PRACTICAL" implies that the paper reports on a research effort wherein a certain piece of software plays an important role (e.g., a novel user interface idea might be supported by a software application demonstrating that idea), whereas our paper is actually associated with a mechanically verified mathematical model of a language and some proofs of properties of that model.  Hence, it is not unlikely that most people would choose "THEORETICAL" to describe the paper.
SURVEY:AUTHOR1:CORRECT_CODE_LOCATION[string] 
SURVEY:AUTHOR1:PUBLIC_COMMENT[string] Thanks for doing a repeatability study, we should have more of them!
SURVEY:AUTHOR1:PUBLISHED_CODE[not_applicable, yes, no] yes
SURVEY:AUTHOR1:SAME_VERSION[not_applicable, yes, no_but_available, no_and_not_available] yes
SURVEY:AUTHOR1:SAME_VERSION_COMMENT[string] 
SURVEY:AUTHOR1:STUDY_FOUND_CORRECT_CODE[not_applicable, yes, no] yes
SURVEY:AUTHOR2:BUILD_COMMENT[string] 
SURVEY:AUTHOR2:BUILD_DIFFICULTY[not_applicable, reasonable_effort, code_problematic or string] reasonable_effort
SURVEY:AUTHOR2:BUILD_DIFFICULTY_COMMENT[string] 
SURVEY:AUTHOR2:CLASSIFICATION[practical,theoretical,hardware] practical
SURVEY:AUTHOR2:CLASSIFICATION_COMMENT[string] 
SURVEY:AUTHOR2:CORRECT_CODE_LOCATION[string] 
SURVEY:AUTHOR2:PUBLIC_COMMENT[string] The examples for our calculus are provided with the proof. There is no need for any extra effort for "executing" the examples. If proof and the examples build, the examples have typechecked correctly.
SURVEY:AUTHOR2:PUBLISHED_CODE[not_applicable, yes, no] yes
SURVEY:AUTHOR2:SAME_VERSION[not_applicable, yes, no_but_available, no_and_not_available] yes
SURVEY:AUTHOR2:SAME_VERSION_COMMENT[string] 
SURVEY:AUTHOR2:STUDY_FOUND_CORRECT_CODE[not_applicable, yes, no] yes