From 3dad2e7284ad22c0fffe293ef4af8a9c46657868 Mon Sep 17 00:00:00 2001 From: Ian Voysey Date: Tue, 1 Nov 2016 10:40:36 -0400 Subject: [PATCH 1/3] adding link to reviews --- README.md | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/README.md b/README.md index a87b091..985be6c 100644 --- a/README.md +++ b/README.md @@ -1,7 +1,10 @@ # agda-popl17 This repository contains the mechanization of Hazelnut and the associated -metatheory as submitted to POPL 2017 for artifact evaluation. +metatheory as submitted to POPL 2017 for artifact evaluation. This artifact +passed evaluation with high marks. The +[reviews](https://github.com/hazelgrove/hazelnut-popl17/blob/master/hazelnut-popl17-aec-reviews.txt) +from the AEC can be found on the repo for the paper text. The branch `sums` is the mechanization of the core calculus extended with sum types as described in Section 4 of the paper. It's a conservative From 48633e039b41a73106dcb35edc7c2c821312c385 Mon Sep 17 00:00:00 2001 From: Ian Voysey Date: Tue, 1 Nov 2016 10:57:05 -0400 Subject: [PATCH 2/3] Removing link to reviews --- README.md | 5 +---- 1 file changed, 1 insertion(+), 4 deletions(-) diff --git a/README.md b/README.md index 985be6c..a87b091 100644 --- a/README.md +++ b/README.md @@ -1,10 +1,7 @@ # agda-popl17 This repository contains the mechanization of Hazelnut and the associated -metatheory as submitted to POPL 2017 for artifact evaluation. This artifact -passed evaluation with high marks. The -[reviews](https://github.com/hazelgrove/hazelnut-popl17/blob/master/hazelnut-popl17-aec-reviews.txt) -from the AEC can be found on the repo for the paper text. +metatheory as submitted to POPL 2017 for artifact evaluation. The branch `sums` is the mechanization of the core calculus extended with sum types as described in Section 4 of the paper. It's a conservative From a74be66358acf89c89c3ead49c3a5a58ce8230f3 Mon Sep 17 00:00:00 2001 From: Ian Voysey Date: Wed, 2 Nov 2016 15:59:00 -0400 Subject: [PATCH 3/3] updated readme to remove some ambiguous and incorrect text point out by a reviewer. cross referenced with Carlo to try to make sure I got it right this time. --- README.md | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/README.md b/README.md index a87b091..a4545ad 100644 --- a/README.md +++ b/README.md @@ -210,16 +210,16 @@ Assumptions and Representation Decisions obfuscating the proof text. One concern with this representation is whether or not it's really - constructive: there are some theorems about contexts that are only about - this representation if you have function extensionality, which amounts to - the Axiom of Choice. + constructive: there are some theorems about contexts that are only + provably about this representation if you have function extensionality, + which is independent from the logic of Agda. In this case, however, the functions that we build as contexts always - have a finite domain and codomain, so that concern is not as bad as it - might be. That fact is not reflected in the type of contexts. It could be - made explicit by using mappings from `Fin n → τ̇` or paired with a - maximum-name-used-so-far. We have not needed to do that yet, but it is an - easy refactoring if we do in the future. + have a finite domain and codomain. Function extensionality is provable + under that restriction, but the restriction is not reflected in the type + of contexts. It could be made explicit by using mappings from `Fin n → τ̇` + or paired with a maximum-name-used-so-far. We have not needed to do that + yet, but it is an easy refactoring if we do in the future. - The notion of consistency that we inherit from the work on gradual typing is deliberately not transitive, so it can't be gracefully encoded with