diff --git a/papers/scp/conflicts b/papers/scp/conflicts deleted file mode 100644 index 16a75691..00000000 --- a/papers/scp/conflicts +++ /dev/null @@ -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) diff --git a/papers/scp/highlights.txt b/papers/scp/highlights.txt new file mode 100644 index 00000000..09df6539 --- /dev/null +++ b/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.