From d43d918486d4e2e6da9a9eaab8590f071cc1d1c0 Mon Sep 17 00:00:00 2001
From: Ben Greenman <benjaminlgreenman@gmail.com>
Date: Sun, 22 May 2016 17:59:14 -0400
Subject: [PATCH] [popl-2017] on your marks
---
icfp-2016/README.md | 2 ++
popl-2017/pre-popl/.gitignore | 11 ++++++
popl-2017/pre-popl/Makefile | 2 ++
popl-2017/pre-popl/pre-popl.scrbl | 56 +++++++++++++++++++++++++++++++
4 files changed, 71 insertions(+)
create mode 100644 popl-2017/pre-popl/.gitignore
create mode 100644 popl-2017/pre-popl/Makefile
create mode 100644 popl-2017/pre-popl/pre-popl.scrbl
diff --git a/icfp-2016/README.md b/icfp-2016/README.md
index 5d033f0..76967f1 100644
--- a/icfp-2016/README.md
+++ b/icfp-2016/README.md
@@ -1,3 +1,5 @@
trivial @ icfp 2016, hopefully
---
+NOPE
+
diff --git a/popl-2017/pre-popl/.gitignore b/popl-2017/pre-popl/.gitignore
new file mode 100644
index 0000000..2c09e77
--- /dev/null
+++ b/popl-2017/pre-popl/.gitignore
@@ -0,0 +1,11 @@
+*.aux
+*.bbl
+*.blg
+*.cls
+*.log
+*.out
+*.pdf
+
+*.css
+*.html
+*.js
diff --git a/popl-2017/pre-popl/Makefile b/popl-2017/pre-popl/Makefile
new file mode 100644
index 0000000..6753aff
--- /dev/null
+++ b/popl-2017/pre-popl/Makefile
@@ -0,0 +1,2 @@
+all:
+ scribble --html pre-popl.scrbl
diff --git a/popl-2017/pre-popl/pre-popl.scrbl b/popl-2017/pre-popl/pre-popl.scrbl
new file mode 100644
index 0000000..37d1c42
--- /dev/null
+++ b/popl-2017/pre-popl/pre-popl.scrbl
@@ -0,0 +1,56 @@
+#lang scribble/manual
+
+@title{Do You See What I See, in review}
+
+Rejected at ICFP, making ready for a POPL submission.
+
+
+@section{SoundX}
+@subsection{What is SoundX?}
+
+@hyperlink["http://conf.researchr.org/event/POPL-2016/popl-2016-papers-sound-type-dependent-syntactic-language-extension"]{SoundX} is a system for:
+@itemlist[
+ @item{
+ @emph{Modeling} programming languages.
+ }
+ @item{
+ Writing type-sound extensions to a base language.
+ The extensions are new type derivations expressed in terms of the base language's type system.
+ }
+]
+
+@; TODO possible to run soundx programs?
+
+@subsection{Key Features of SoundX}
+@itemlist[
+ @item{
+ Proposes a new idea: desugarings act on type derivations are are guaranteed
+ to produce only well-typed terms.
+ }
+ @item{
+ Detailed metatheory (may be useful reference for others)
+ }
+ @item{
+ Models a subset of Java and implements Scala-inspired extensions.
+ (Everyone loves Java and nobody @emph{really} trusts Scala.)
+ }
+]
+
+@subsection{Lessons from SoundX}
+@itemlist[
+ @item{
+ Errors must be reported in terms of the source language, not the desugared result
+ }
+ @item{
+ Type errors in code produced by a desugaring must reflect USER type errors,
+ not errors in the desugaring rules.
+ }
+ @item{
+ Desugarings should have access to type information.
+ }
+]
+
+
+@section{Our Contribution}
+
+