Added highlights

papers/scp/conflicts

@@ -1,46 +0,0 @@
-All (Indiana University)
-Giuseppe Castagna (Univ. of Paris Diderot)
-David Broman (KTH)
-Amal Ahmed (Northeastern Univ.)
-Dustin Jamner (Northeastern Univ.)
-Michael M. Vitousek (Facebook)
-Matteo Cimini (Univ. of Mass. Lowell)
-Carl Friedrich Bolz-Tereick (Heinrich-Heine-Universität Düsseldorf)
-David Christiansen (Galois Inv.)
-Peter Thiemann (Univ. of Freiburg)
-All (University of Edinburgh)
-Fabrizio Montesi (University of Southern Denmark)
-Marco Peressotti (University of Southern Denmark)
-J. Garrett Morris (Kansas University)
-All (University of Edinburgh)
-J. Garrett Morris (Kansas University)
-Jeremy Yallop (Cambridge)
-Jack Williams (Microsoft)
-Jakub Zalewski
-Shayan Najd
-Niki Vazou (IMDEA Software Institute)
-Anish Tondwalkar  (University of California, San Diego)
-Vikram Choudhury (Indiana University)
-Ryan G. Scott (Indiana University)
-Ryan R. Newton (Indiana University)
-Ranjit Jhala (University of California, San Diego)
-Atsushi Igarashi (Kyoto University)
-Vasco T. Vasconcelos (University of Lisbon)
-Tom Schrijvers (KU Leuven)
-Bruno Oliveira (University of Hong Kong)
-Koar Mantirosian (KU Leuven)
-Marco Carbone (IT University of Copenhagen)
-Fabrizio Montesi (University of Southern Denmark)
-Carsten Schürmann (IT University of Copenhagen)
-Andreas Abel (Gothenburg University)
-Jesper Cockx (Gothenburg University)
-Dominique Devriese (Vrije Universiteit Brussel)
-Amin Timany (KU~Leuven)
-Nobuko Yoshida (Imperial)
-Raymond Hu (Hertfordshire)
-Bernardo Toninho (Universidade NOVA de Lisboa)
-Julien Lange (Kent)
-Simon Thompson (Kent)
-Nicholas Ng
-Robert Griesemer (Google)
-All (IOHK)

papers/scp/highlights.txt

@@ -0,0 +1,20 @@
+Highlights for Review
+
+* PLFA is an online textbook, available at
+
+    plfa.inf.ed.ac.uk
+
+* The proofs for a textbook on programming
+  languages can be written in Agda,
+  without a separate scripting language.
+
+* Constructive proofs of preservation and
+  progress give rise to a prototype evaluator.
+
+* Using raw terms with a separate typing
+  relation is far less perspicuous than using
+  inherently-typed terms.
+
+* An online final examination with access to a
+  proof assistant can lead to flawless student
+  performance.