Filter Program
Conference Dates
Conference Dates are in time zone (GMT+01:00) Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna, and may differ from the viewed time zone.
Rooms
Tracks
Badges
Your Program
Conference DaySun 15 JanDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
Conference Day
Sun 15 JanDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
08:50 - 10:00 | |||
08:50 10mDay opening | Welcome TTT | ||
09:00 20mTalk | A Case Study in Programming Coinductive Proofs in Beluga: Howe's Method TTT | ||
09:20 20mTalk | Needle & Knot: A Framework for Meta-Theoretical Specifications with Binding TTT | ||
09:40 20mTalk | Equivalence of System F and λ2 in Abella TTT | ||
09:00 - 10:00 | |||
09:00 60mTalk | Detecting Strict Aliasing Violations in the Wild VMCAI Pascal CuoqTrust-in-Soft File Attached | ||
09:15 - 10:00 | |||
09:15 45mTalk | What is Secure Compilation? Part I SCM Marco PatrignaniMPI-SWS, Germany Link to publication | ||
10:00 - 10:30 | |||
10:00 30mCoffee break | Break Catering | ||
10:30 - 12:00 | |||
10:30 30mTalk | Partitioned Memory Models for Program Analysis. VMCAI File Attached | ||
11:00 30mTalk | Property Directed Reachability for Proving Absence of Concurrent Modification Errors VMCAI Asya FrumkinTel Aviv University, Yotam M. Y. FeldmanTel Aviv University, Ondřej LhotákUniversity of Waterloo, Canada, Oded PadonTel Aviv University, Mooly SagivTel Aviv University, Sharon ShohamTel Aviv university File Attached | ||
11:30 30mTalk | Stabilizing Floating-Point Programs using Provenance Analysis VMCAI | ||
10:30 - 12:00 | |||
10:30 50mTalk | Invited Talk -- Type Theory in the Software Analysis Workbench TTT Aaron TombGalois, Inc. | ||
11:20 20mTalk | Modelling Program Behaviour within Software Verification Tool LAV TTT | ||
11:40 20mTalk | agdARGS - Declarative Hierarchical Command Line Interfaces TTT Guillaume AllaisRadboud University Nijmegen | ||
10:30 - 12:00 | |||
10:30 10mTalk | What is Secure Compilation? Part II (Short talk) SCM Cătălin HriţcuInria Paris Link to publication | ||
10:40 10mTalk | Can relational logic facilitate secure compilation? (Short talk) SCM David NaumannStevens Institute of Technology File Attached | ||
10:50 10mTalk | Full Abstraction for Language Design (Short talk) SCM Gabriel SchererNortheastern University File Attached | ||
11:00 10mTalk | Cogent: Where we Stand and What Comes Next (Short talk) SCM Christine RizkallahUniversity of Pennsylvania, USA File Attached | ||
11:15 45mTalk | Enforcing Well-Bracketed Control Flow on a Capability Machine using Local Capabilities SCM File Attached | ||
12:00 - 14:00 | |||
12:00 2hLunch | Lunch Catering | ||
14:00 - 15:30 | |||
14:00 30mTalk | Accuracy of Message Counting Abstraction in Fault-Tolerant Distributed Algorithms VMCAI | ||
14:30 30mTalk | Independence Abstractions and Models of Concurrency VMCAI | ||
15:00 30mTalk | Static Analysis of Communicating Process using Symbolic Transducers VMCAI Vincent BotbolCEA LIST + LIP6 Université Pierre & Marie Curie, Tristan Le GallCEA LIST, Emmanuel ChaillouxLIP6 - UPMC Media Attached File Attached | ||
14:00 - 15:30 | |||
14:00 50mTalk | Invited Talk -- Cubical Type Theory: a constructive interpretation of the univalence axiom TTT Anders MörtbergInria | ||
14:50 20mTalk | Equations: a tool for dependent pattern-matching TTT File Attached | ||
15:10 20mTalk | Coq's Prolog and application to defining semi-automatic tactics TTT File Attached | ||
14:00 - 15:30 | |||
14:00 45mTalk | Linking Types: Secure compilation of multi-language programs SCM Daniel PattersonNortheastern University File Attached | ||
14:45 45mTalk | Fully-Abstract Compilation of Parametric Polymorphism into Dynamic Sealing SCM Dominique DevrieseiMinds - Distrinet, KU Leuven File Attached | ||
15:30 - 16:00 | |||
15:30 30mCoffee break | Break Catering | ||
16:00 - 17:30 | Decision proceduresVMCAI at Amphitheater 44 Chair(s): Andreas PodelskiUniversity of Freiburg, Germany | ||
16:00 30mTalk | Synthesising Strategy Improvement and Recursive Algorithms for Solving 2.5 Player Parity Games VMCAI Ernst Moritz HahnState Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Sven ScheweUniversity of Liverpool, Andrea TurriniState Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Lijun ZhangInstitute of Software, Chinese Academy of Sciences File Attached | ||
16:30 30mTalk | Reasoning in the Bernays-Schönfinkel-Ramsey Fragment of Separation Logic VMCAI Andrew ReynoldsEPFL, Radu IosifVERIMAG, CNRS, Université Grenoble-Alpes, Cristina SerbanVERIMAG, CNRS, Université Grenoble-Alpes File Attached | ||
17:00 30mTalk | Matching multiplications in Bit-Vector formulas VMCAI File Attached | ||
16:00 - 18:00 | |||
16:00 50mTalk | Invited Talk -- Iris: a framework for higher-order concurrent separation logic in Coq TTT Robbert KrebbersDelft University of Technology, Netherlands | ||
16:50 20mTalk | Introducing MetaCoq: A Safe Tactic Language for Coq TTT Beta ZilianiFAMAF, UNC (Argentina) / CONICET (Argentina) | ||
17:10 50mOther | COST EUTypes session TTT | ||
16:00 - 17:30 | |||
16:00 45mTalk | Software Fault Isolation avec CompCert SCM File Attached | ||
16:45 45mTalk | Security preserving compilation of low-level programs embedded in F* SCM Jonathan ProtzenkoMicrosoft Research File Attached | ||
Conference DayMon 16 JanDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
Conference Day
Mon 16 JanDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
08:50 - 09:00 | Opening remarksPADL at Salle 116, Barre 44-54 Chair(s): Yuliya LierlerUniversity of Nebraska, Walid TahaHalmstad University | ||
08:50 10mTalk | Opening remarks PADL | ||
09:00 - 10:00 | |||
09:00 60mTalk | Verified Concurrent Code: Tricks of the Trade VMCAI | ||
09:00 - 10:00 | |||
09:00 60mTalk | Porting the HOL Light Analysis Library: Some Lessons CPP Lawrence PaulsonUniversity of Cambridge File Attached | ||
09:00 - 12:00 | |||
09:00 3hTalk | The State of the Art in Gradual Typing Tutorials Jeremy G. SiekIndiana University Bloomington | ||
09:00 - 12:00 | |||
09:00 3hTalk | The Lean Theorem Prover Tutorials Leonardo de MouraMicrosoft Research, Redmond, Gabriel EbnerVienna University of Technology, Jared RoeschUniversity of Washington, USA, Sebastian UllrichKarlsruhe Institute of Technology | ||
09:00 - 10:00 | |||
09:00 60mTalk | Compiling Untyped Lambda Calculus to Lower-Level Code by Game Semantics and Partial Evaluation (Invited Talk) PEPM DOI | ||
09:00 - 12:00 | |||
09:00 3hTalk | Fast and Precise Type Checking for JavaScript: Are you in Flow? Tutorials Avik ChaudhuriFacebook Media Attached | ||
09:00 - 12:00 | |||
09:00 3hTalk | Let's Implement Your New Analysis using Industrially Strengthened Frama-C Plugins Tutorials | ||
09:00 - 10:00 | |||
09:00 60mTalk | Proof checking and logic programming PADL Dale MillerINRIA Saclay and LIX | ||
10:00 - 10:30 | |||
10:00 30mCoffee break | Break Catering | ||
10:30 - 12:00 | |||
10:30 30mTalk | Sound Bit-Precise Numerical Domains VMCAI Tushar SharmaUniversity of Wisconsin - Madison, USA, Thomas RepsUniversity of Wisconsin - Madison and Grammatech Inc. File Attached | ||
11:00 30mTalk | Efficient Elimination of Redundancies in Polyhedra using Raytracing VMCAI Media Attached File Attached | ||
11:30 30mTalk | Finding Relevant Templates via the Principal Component Analysis VMCAI Yassamine SeladjiUniversity of Tlemcen File Attached | ||
10:30 - 12:00 | |||
10:30 30mTalk | Verifying a hash table and its iterators in higher-order separation logic CPP | ||
11:00 30mTalk | A Formalization of the Berlekamp-Zassenhaus Factorization Algorithm CPP | ||
11:30 30mTalk | Formal foundations of 3D geometry for modeling robot manipulators CPP | ||
10:30 - 12:00 | |||
10:30 30mTalk | Lightweight Soundness for Towers of Language Extensions PEPM | ||
11:00 30mTalk | Detecting code clones with gaps by function applications PEPM | ||
11:30 30mTalk | PEG Parsing in Less Space Using Progressive Tabling and Dynamic AnalysisBest Paper PEPM | ||
10:30 - 12:00 | |||
10:30 30mTalk | Lowering the learning curve for declarative programming: a Python API for the IDP system PADL Joost VennekensKU Leuven | ||
11:00 30mTalk | Extending Answer Set Programs with Interpreted Functions as First-class Citizens PADL Christoph RedlVienna University of Technology | ||
11:30 30mTalk | Integrating Answer Set Programming with Object-oriented Languages PADL | ||
12:00 - 14:00 | |||
12:00 2hLunch | Lunch Catering | ||
14:00 - 15:30 | Model-checking and bug findingVMCAI at Amphitheater 44 Chair(s): Andreas PodelskiUniversity of Freiburg, Germany | ||
14:00 30mTalk | Effective Bug Finding in C Programs with Shape and Effect Abstraction VMCAI Iago AbalIT University of Copenhagen, Claus BrabrandIT University of Copenhagen, Denmark, Andrzej WąsowskiIT University of Copenhagen, Denmark | ||
14:30 30mTalk | Reduction of Workflow Nets for Generalised Soundness Verification VMCAI Hadrien BrideFemto-ST / Université de Franche-Comté, Olga KouchnarenkoFemto-ST / Université de Franche-Comté, Fabien PeureuxFemto-ST / Université de Franche-Comté + Smartesting S&S Media Attached | ||
15:00 30mTalk | Dynamic Reductions for Model Checking Concurrent Software. VMCAI Henning GüntherTechnische Universität Wien, Alfons LaarmanVienna University of Technology, Ana SokolovaUniversity of Salzburg, Georg WeissenbacherTechnische Universität Wien File Attached | ||
14:00 - 15:30 | |||
14:00 30mTalk | BliStrTune: Hierarchical Invention of Theorem Proving Strategies CPP | ||
14:30 30mTalk | Automatic Cyclic Termination Proofs for Recursive Procedures in Separation Logic CPP | ||
15:00 30mTalk | Formalization of Karp-Miller Tree Construction on Petri Nets CPP | ||
14:00 - 17:00 | |||
14:00 3hTalk | The State of the Art in Gradual Typing Tutorials Jeremy G. SiekIndiana University Bloomington | ||
14:00 - 17:00 | |||
14:00 3hTalk | The Lean Theorem Prover Tutorials Leonardo de MouraMicrosoft Research, Redmond, Gabriel EbnerVienna University of Technology, Jared RoeschUniversity of Washington, USA, Sebastian UllrichKarlsruhe Institute of Technology | ||
14:00 - 15:30 | Tutorial (Idris, Inside-Out) and Poster SessionPEPM at Salle 109, Barre 44-54 Chair(s): Ulrik Pagh SchultzUniversity of Southern Denmark, Jeremy YallopUniversity of Cambridge, UK | ||
14:00 60mTalk | Idris, Inside-Out: A Tutorial on Extending Idris in Idris PEPM David Thrane ChristiansenIndiana University | ||
15:00 30mTalk | Invited posters PEPM Nada AminEPFL, Tiark RompfPurdue University, Oleg Kiselyov, Aggelos BiboudisUniversity of Athens, Nick PalladinosNessos Information Technologies, SA, Yannis SmaragdakisUniversity of Athens | ||
15:00 30mTalk | Language-integrated Query with Ordering, Grouping and Outer Joins (poster) PEPM | ||
14:00 - 17:00 | |||
14:00 3hTalk | Fast and Precise Type Checking for JavaScript: Are you in Flow? Tutorials Avik ChaudhuriFacebook Media Attached | ||
14:00 - 17:00 | |||
14:00 3hTalk | Let's Implement Your New Analysis using Industrially Strengthened Frama-C Plugins Tutorials | ||
14:00 - 15:30 | |||
14:00 30mTalk | Failing Faster: Overlapping Patterns for Property-Based Testing PADL | ||
14:30 30mTalk | Boltzmann Samplers for Closed Simply-Typed Lambda Terms PADL Maciej BendkowskiJagiellonian University, Katarzyna GrygielJagiellonian University, Paul TarauUniversity of North Texas | ||
15:00 30mTalk | Selection Equilibria of Higher-Order Games PADL Paulo OlivaQueen Mary University of London, Jules HedgesUniversity of Oxford, Viktor WinschelETH Zürich, Philipp ZahnUniversity of St. Gallen, Evguenia ShpritsUniversity of Mannheim | ||
15:30 - 16:00 | |||
15:30 30mCoffee break | Break Catering | ||
16:00 - 17:30 | Symbolic analysis and invariant synthesisVMCAI at Amphitheater 44 Chair(s): Constantin EneaLIAFA, Université Paris Diderot | ||
16:00 30mTalk | Block-wise abstract interpretation by combining abstract domains with SMT VMCAI | ||
16:30 30mTalk | IC3 - Flipping the E in ICE VMCAI Yakir Vizel, Arie GurfinkelUniversity of Waterloo, Sharon ShohamTel Aviv university, Sharad MalikPrinceton University | ||
17:00 30mTalk | Counterexample Validation and Interpolation-Based Refinement for Forest Automata VMCAI Lukáš Holík, Martin HruskaBrno University of Technology , Ondřej LengálBrno University of Technology , Adam RogalewiczBrno University of Technology , Tomáš VojnarBrno University of Technology | ||
16:00 - 18:00 | |||
16:00 30mTalk | A Coq Formal Proof of the Lax–Milgram theorem CPP | ||
16:30 30mTalk | A Reflexive Tactic for Polynomial Positivity using Numerical Solvers and Floating-Point Computations CPP | ||
17:00 30mTalk | Markov Processes in Isabelle/HOL CPP Johannes HölzlTechnische Universität München DOI Pre-print File Attached | ||
17:30 30mTalk | Formalising Real Numbers in Homotopy Type Theory CPP | ||
16:00 - 17:00 | Transformation (part I)PEPM at Salle 109, Barre 44-54 Chair(s): Chung-chieh ShanIndiana University, USA | ||
16:00 30mTalk | Verification of Code Generators via Higher-Order Model Checking PEPM Takashi SuwaUniversity of Tokyo, Japan, Takeshi TsukadaUniversity of Tokyo, Japan, Naoki KobayashiUniversity of Tokyo, Japan, Atsushi IgarashiKyoto University | ||
16:30 30mTalk | Interactive data representation migration: Exploiting program dependence to aid program transformation PEPM | ||
16:00 - 17:30 | |||
16:00 30mTalk | A Domain-Specific Language for Software-Defined Radio PADL Geoffrey MainlandDrexel University | ||
16:30 30mTalk | A Declarative DSL for Customized Rendering of Text-Based Art PADL | ||
17:00 30mTalk | Using Iterative Deepening for Probabilistic Logic Inference PADL | ||
Conference DayTue 17 JanDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
Conference Day
Tue 17 JanDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
08:50 - 09:00 | |||
08:50 10mDay opening | Welcome Sesssion PLMW | ||
09:00 - 10:00 | |||
09:00 60mTalk | Verification of Cancer Programs VMCAI Jasmin FisherMicrosoft Research | ||
09:00 - 10:00 | |||
09:00 60mTalk | Mechanized verification of preemptive OS kernels CPP Xinyu FengUniversity of Science and Technology of China File Attached | ||
09:00 - 10:00 | |||
09:00 60mTalk | Towards a metric semantics for probabilistic programming (invited talk) PPS | ||
09:00 - 10:00 | |||
09:00 30mTalk | Time management, family and quality of life PLMW Kathleen FisherTufts University File Attached | ||
09:30 30mTalk | Abductive Reasoning in Deductive Verification PLMW Isil DilligUT Austin File Attached | ||
09:00 - 10:00 | Tutorial: reversible computingPEPM at Salle 109, Barre 44-54 Chair(s): Ulrik Pagh SchultzUniversity of Southern Denmark | ||
09:00 60mTalk | Reversible computing from a programming language perspective PEPM | ||
09:00 - 10:00 | |||
09:00 30mTalk | Funky Grooves: Declarative Programming of Full-Fledged Musical Applications PADL | ||
09:30 30mTalk | DALI for Cognitive Robotics: Principles and Prototype Implementation PADL Stefania CostantiniDipartimento di Ingegneria e Scienze dell'Informazione eMatematica, Univ. dell'Aquila, Giovanni De GasperisDipartimento di Ingegneria e Scienze dell'Informazione eMatematica, Giulio NazziconeDipartimento di Ingegneria e Scienze dell'Informazione eMatematica | ||
10:00 - 10:30 | |||
10:00 30mCoffee break | Break Catering | ||
10:30 - 12:00 | Model Checking and SynthesisVMCAI at Amphitheater 44 Chair(s): Ahmed BouajjaniIRIF, Université Paris Diderot | ||
10:30 30mTalk | Reachability for dynamic parametric processes VMCAI Anca MuschollUniversité de Bordeaux / LaBRI, Helmut SeidlTechnische Universität München, Igor WalukiewiczCNRS, LaBRI | ||
11:00 30mTalk | Synthesizing Non-Vacuous Systems VMCAI Roderick BloemInstitute of Software Technology, Graz University of Technology , Hana Chockler, Masoud EbrahimiInstitute of Applied Information Processing and Communications, Graz University of Technology, Ofer StrichmanTechnion File Attached | ||
11:30 30mTalk | Solving Nonlinear Integer Arithmetic with MCSat VMCAI Dejan JovanovićSRI International | ||
10:30 - 12:00 | |||
10:30 30mTalk | Verified compilation of CakeML to multiple machine-code targets CPP Anthony FoxUniversity of Cambridge, UK, Magnus O. MyreenChalmers University of Technology, Sweden, Yong Kiam TanIHPC at A*STAR, Singapore, Ramana Kumar | ||
11:00 30mTalk | COMPLX: a verification framework for concurrent imperative programs CPP Sidney AmaniUNSW, Australia, June AndronickData61,CSIRO (formerly NICTA) and UNSW, Maksym Bortin, Corey Lewis, Christine RizkallahUniversity of Pennsylvania, USA, Joseph Tuong | ||
11:30 30mTalk | Verifying dynamic race detection CPP William ManskyUniversity of Pennsylvania, Yuanfeng PengUniversity of Pennsylvania, Steve ZdancewicUniversity of Pennsylvania, Joseph DeviettiUniversity of Pennsylvania | ||
10:30 - 12:00 | |||
10:30 20mTalk | An application of computable distributions to the semantics of probabilistic programs: part 2 PPS | ||
10:50 10mMeeting | Discussion 1 PPS | ||
11:00 20mTalk | Probabilistic programming and a domain theoretic approach to Skorohod's theorem PPS Michael MisloveTulane | ||
11:20 10mMeeting | Discussion 2 PPS | ||
11:30 20mTalk | Building inference algorithms from monad transformers PPS Adam ŚcibiorUniversity of Cambridge, Yufei CaiUniversity of Tübingen, Germany, Klaus OstermannUniversity of Tübingen, Germany, Zoubin GhahramaniUniversity of Cambridge | ||
11:50 10mMeeting | Discussion 3 PPS | ||
10:30 - 12:00 | |||
10:30 30mTalk | What is research and how to do it? Thinking globally and acting locally. PLMW Michael HicksUniversity of Maryland at College Park, USA File Attached | ||
11:00 30mTalk | Mechanizing Meta-Theory in Beluga PLMW Brigitte PientkaMcGill University File Attached | ||
11:30 30mTalk | Research: The Industrial Culture PLMW Nikhil SwamyMicrosoft Research File Attached | ||
10:30 - 12:00 | |||
10:30 30mTalk | Cost versus Precision for Approximate Typing for Python PEPM | ||
11:00 30mTalk | Refining types using type guards in TypeScript PEPM | ||
11:30 30mTalk | Predicting Resource Consumption of Higher-Order Workflows PEPM Markus KlinikRadboud University Nijmegen, Jurriaan HageUtrecht University, Jan Martin JansenNetherlands Defence Academy, Rinus PlasmeijerRadboud University Nijmegen | ||
10:30 - 12:00 | |||
10:30 30mTalk | Improving Non-deterministic Computations in Functional Logic Programs PADL | ||
11:00 30mTalk | Canonicalizing High-Level Constructs in Picat PADL | ||
11:30 30mTalk | An Overview of PRhoLog PADL Besik DunduaInstitute of Applied Mathematics, Tbilisi State University, Temur Kutsia, Klaus Reisenberger-HagmayerJohannes Kepler University Linz | ||
12:00 - 14:00 | |||
12:00 2hLunch | Lunch Catering | ||
14:00 - 15:30 | Abstract InterpretationVMCAI at Amphitheater 44 Chair(s): Roberto GiacobazziUniversity of Verona, Italy | ||
14:00 30mTalk | Complete Abstractions and Subclassical Modal Logics VMCAI | ||
14:30 30mTalk | Structuring Abstract Interpreters through State and Value Abstractions VMCAI Media Attached | ||
15:00 30mTalk | Conjunctive Abstract Interpretation using Paramodulation VMCAI Mooly SagivTel Aviv University, A: Or OzeriTel Aviv university, Oded PadonTel Aviv University, Noam RinetzkyTel Aviv University Media Attached | ||
14:00 - 15:30 | |||
14:00 30mTalk | The HoTT library: a formalization of homotopy type theory in Coq CPP Andrej BauerUniversity of Ljubljana, Jason GrossMIT CSAIL, Peter Lefanu Lumsdaine, Michael Shulman, Matthieu SozeauInria, Bas Spitters Pre-print | ||
14:30 30mTalk | Lifting proof-relevant unification to higher dimensions CPP | ||
15:00 30mTalk | The Next 700 Syntactical models of type theory CPP | ||
14:00 - 15:30 | |||
14:00 20mTalk | Commutativity logic for probabilistic trace equivalence: complete or not? PPS | ||
14:20 10mMeeting | Discussion 4 PPS | ||
14:30 20mTalk | Mathematical structures of probabilistic programming PPS Ilias GarnierUniversity of Edinburgh, Fredrik DahlqvistUniversity College London, Florence ClercMcGill University, Vincent DanosENS Paris/CNRS | ||
14:50 10mMeeting | Discussion 5 PPS | ||
15:00 20mTalk | A weakest pre-expectation semantics for mixed-sign expectations PPS | ||
15:20 10mMeeting | Discussion 6 PPS | ||
14:00 - 15:30 | |||
14:00 60mTalk | Student Interaction Activity PLMW Eva DarulovaMPI-SWS, Loris D'AntoniUniversity of Wisconsin–Madison, Alexandra SilvaUniversity College London, Dimitrios VytiniotisMicrosoft Research, Cambridge | ||
15:00 30mTalk | How to Give Talks That People Can Follow PLMW Derek DreyerMPI-SWS File Attached | ||
14:00 - 15:30 | Tutorial: Partial Evaluation for Language ImplementationPEPM at Salle 109, Barre 44-54 Chair(s): Jeremy YallopUniversity of Cambridge, UK | ||
14:00 90mTalk | Practical Partial Evaluation for Language Implementation with Graal & Truffle PEPM | ||
15:30 - 16:00 | |||
15:30 30mCoffee break | Break Catering | ||
16:00 - 17:30 | |||
16:00 30mTalk | Using Abstract Interpretation to Correct Synchronization Faults VMCAI Pietro FerraraIBM Research, Omer TrippIBM Thomas J. Watson Research Center, Peng LiuPurdue University, Eric KoskinenYale University | ||
16:30 30mTalk | Detecting All High-Level Dataraces in an RTOS Kernel. VMCAI | ||
17:00 30mTalk | Precise Thread-Modular Abstract Interpretation of Concurrent Programs using Relational Interference Abstractions VMCAI | ||
16:00 - 17:30 | |||
16:00 30mTalk | Type-and-scope safe programs and their proofs CPP Guillaume AllaisRadboud University Nijmegen, James Chapman, Conor McBride, James McKinnaUniversity of Edinburgh | ||
16:30 30mTalk | Formally verified differential dynamic logic CPP | ||
17:00 30mTalk | Equivalence of System F and λ2 in Coq based on context morphism lemmas CPP | ||
16:00 - 18:00 | |||
16:00 30mTalk | Machine Learning and Programming Languages: latest directions and research opportunities PLMW Martin VechevETH Zurich File Attached | ||
16:30 30mTalk | The Curse of Knowledge PLMW Benjamin C. PierceUniversity of Pennsylvania File Attached | ||
17:00 60mTalk | Young Researcher Panel Session PLMW Roopsha SamantaPurdue University, Nada AminEPFL, Jonathan ProtzenkoMicrosoft Research, Zachary KincaidPrinceton University | ||
16:00 - 17:00 | |||
16:00 30mTalk | Functional Parallels of Sequential Imperatives PEPM | ||
16:30 30mTalk | A Functional Reformulation of UnCAL Graph-Transformations: Or, Graph Transformation as Graph Reduction PEPM | ||
16:30 - 18:00 | |||
16:30 20mTalk | An exponential family basis for probabilistic programming PPS Chad ScherrerGalois, Inc. | ||
16:50 10mMeeting | Discussion 7 PPS | ||
17:00 20mTalk | The semantics of subroutines and iteration in the Bayesian programming language ProBT PPS | ||
17:20 10mMeeting | Discussion 8 PPS | ||
17:30 20mTalk | Exchangeable random process and data abstraction PPS Sam StatonUniversity of Oxford, Hongseok YangUniversity of Oxford, Nathanael L. AckermanHarvard University, Cameron FreerGamalon and Borelian, Daniel Roy | ||
17:50 10mMeeting | Discussion 9 PPS | ||
18:15 - 19:15 | |||
18:15 20mTalk | Reducing probabilistic choice to nondeterministic choice PPS Ernie CohenAmazon Web Services | ||
18:35 10mMeeting | Discussion 10 PPS | ||
18:45 20mTalk | GraPPa: spanning the expressivity vs. efficiency continuum PPS Edwin WestbrookGalois, Inc., Chad ScherrerGalois, Inc., Nathan CollinsGalois, Inc., Eric MertensGalois, Inc. | ||
19:05 10mMeeting | Discussion 11 PPS | ||
Conference DayWed 18 JanDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
Conference Day
Wed 18 JanDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
09:00 - 09:05 | OpeningPOPL at Auditorium Chair(s): Giuseppe CastagnaParis Diderot University & CNRS, Andrew D. GordonMicrosoft Research and University of Edinburgh | ||
09:00 5mDay opening | Opening POPL | ||
09:05 - 10:00 | Invited speakerPOPL at Auditorium Chair(s): Andrew D. GordonMicrosoft Research and University of Edinburgh | ||
09:05 55mTalk | The Influence of Dependent Types POPL Stephanie WeirichUniversity of Pennsylvania | ||
10:00 - 10:30 | |||
10:00 30mCoffee break | Break Catering | ||
10:30 - 12:10 | Abstract InterpretationPOPL at Amphitheater 44 Chair(s): Isabella MastroeniUniversity of Verona, Italy | ||
10:30 25mTalk | Ogre and Pythia, An invariance proof method for weak consistency models POPL | ||
10:55 25mTalk | A Posteriori Environment Analysis with Pushdown Delta CFA POPL Kimball GermaneUniversity of Utah, Matthew MightUniversity of Utah; Harvard Medical School; The White House | ||
11:20 25mTalk | Semantic-Directed Clumping of Disjunctive Abstract States POPL Huisong LiINRIA/CNRS/ENS/PSL*, François BérengerINRIA/CNRS/ENS/PSL*, Bor-Yuh Evan ChangUniversity of Colorado Boulder, Xavier RivalINRIA/CNRS/ENS Paris | ||
11:45 25mTalk | Fast Polyhedra Abstract Domain POPL | ||
10:30 - 12:10 | |||
10:30 25mTalk | Polymorphism, subtyping and type inference in MLsub POPL | ||
10:55 25mTalk | Java generics are Turing complete POPL Radu GrigoreUniversity of Kent | ||
11:20 25mTalk | Hazelnut: A Bidirectionally Typed Structure Editor Calculus POPL Cyrus OmarCarnegie Mellon University, Ian VoyseyCarnegie Mellon University, Michael HiltonOregon State University, USA, Jonathan AldrichCarnegie Mellon University, Matthew HammerUniversity of Colorado, Boulder | ||
11:45 25mTalk | Modules, Abstraction, and Parametric Polymorphism POPL Karl CraryCarnegie Mellon University | ||
12:10 - 14:20 | |||
12:10 2h10mLunch | Lunch Catering | ||
14:20 - 16:00 | |||
14:20 25mTalk | Beginner's Luck: A Language for Property-Based Generators POPL Leonidas LampropoulosUniversity of Pennsylvania, Diane Gallois-WongInria Paris, ENS Paris, Cătălin HriţcuInria Paris, John HughesChalmers University of Technology, Benjamin C. PierceUniversity of Pennsylvania, Li-yao XiaENS Paris Pre-print | ||
14:45 25mTalk | Exact Bayesian Inference by Symbolic Disintegration POPL Pre-print | ||
15:10 25mTalk | Stochastic Invariants for Probabilistic Termination POPL | ||
15:35 25mTalk | Coupling proofs are probabilistic product programs POPL | ||
14:20 - 16:00 | |||
14:20 25mTalk | A Promising Semantics for Relaxed-Memory Concurrency POPL Jeehoon KangSeoul National University, Chung-Kil HurSeoul National University, Ori LahavMPI-SWS, Viktor VafeiadisMPI-SWS, Germany, Derek DreyerMPI-SWS Link to publication Pre-print Media Attached | ||
14:45 25mTalk | Automatically Comparing Memory Consistency Models POPL John WickersonImperial College London, Mark BattyUniversity of Kent, Tyler SorensenImperial College London, George A. ConstantinidesImperial College London, UK Pre-print Media Attached File Attached | ||
15:10 25mTalk | Interactive Proofs in Higher-Order Concurrent Separation Logic POPL Robbert KrebbersDelft University of Technology, Netherlands, Amin Timanyimec - Distrinet, KU Leuven, Lars BirkedalAarhus University DOI Pre-print Media Attached | ||
15:35 25mTalk | A Relational Model of Types-and-Effects in Higher-Order Concurrent Separation Logic POPL Morten Krogh-JespersenAarhus University, Kasper SvendsenAarhus University, Lars BirkedalAarhus University | ||
16:00 - 16:30 | |||
16:00 30mCoffee break | Break Catering | ||
16:30 - 17:45 | |||
16:30 25mTalk | Monadic second-order logic on finite sequences POPL | ||
16:55 25mTalk | On the Relationship Between Higher-Order Recursion Schemes and Higher-Order Fixpoint Logic POPL Naoki KobayashiUniversity of Tokyo, Japan, Etienne LozesENS Cachan, Florian BruseUniversity of Kassel | ||
17:20 25mTalk | Coming to Terms with Quantified Reasoning POPL Simon RobillardChalmers University of Technology, Andrei VoronkovUniversity of Manchester, Laura KovacsChalmers University of Technology | ||
16:30 - 17:45 | |||
16:30 25mTalk | A Program Optimization for Automatic Database Result Caching POPL | ||
16:55 25mTalk | Stream Fusion, to Completeness POPL Oleg Kiselyov, Aggelos BiboudisUniversity of Athens, Nick PalladinosNessos Information Technologies, SA, Yannis SmaragdakisUniversity of Athens Pre-print Media Attached | ||
17:20 25mTalk | Rigorous Floating-point Mixed Precision Tuning POPL Wei-Fan ChiangSchool of Computing, University of Utah, Ganesh GopalakrishnanUniversity of Utah, Zvonimir RakamaricUniversity of Utah, Ian BriggsSchool of Computing, University of Utah, Marek S. BaranowskiUniversity of Utah, Alexey SolovyevSchool of Computing, University of Utah Pre-print | ||
19:30 - 23:00 | |||
19:30 3h30mDinner | Social dinner Catering | ||
Conference DayThu 19 JanDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
Conference Day
Thu 19 JanDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
09:00 - 09:15 | |||
09:00 5mAwards | Turing Award Video POPL | ||
09:05 5mAwards | Most Influential Paper Award POPL | ||
09:10 5mAwards | Reynolds Doctoral Dissertation Award POPL | ||
09:15 - 10:00 | |||
09:15 45mTalk | 40 Years of Abstract Interpretation — An Interview with Patrick Cousot POPL | ||
10:00 - 10:30 | |||
10:00 30mCoffee break | Break Catering | ||
10:30 - 12:10 | |||
10:30 25mTalk | Relational Cost Analysis POPL Ezgi ÇiçekMPI-SWS, Germany, Gilles BartheIMDEA, Marco GaboardiSUNY Buffalo, USA, Deepak GargMPI-SWS, Germany, Jan HoffmannCarnegie Mellon University | ||
10:55 25mTalk | Contract-based Resource Verification for Higher-order Functions with Memoization POPL | ||
11:20 25mTalk | Context-sensitive data dependence analysis via Linear Conjunctive Language Reachability POPL | ||
11:45 25mTalk | Towards Automatic Resource Bound Analysis for OCaml POPL Jan HoffmannCarnegie Mellon University, Ankush DasCarnegie Mellon University, Shu-chun WengYale University | ||
10:30 - 12:10 | Type Systems 2POPL at Auditorium Chair(s): Andrew D. GordonMicrosoft Research and University of Edinburgh | ||
10:30 25mTalk | Deciding equivalence with sums and the empty type POPL Gabriel SchererNortheastern University | ||
10:55 25mTalk | The exp-log normal form of types: Decomposing extensional equality and representing terms compactly POPL Danko IlikTrusted Labs | ||
11:20 25mTalk | Contextual isomorphisms POPL | ||
11:45 25mTalk | Typed Self-Evaluation via Intensional Type Functions POPL | ||
12:10 - 14:20 | |||
12:10 2h10mLunch | Lunch Catering | ||
14:20 - 16:00 | |||
14:20 25mTalk | Mixed-size Concurrency: ARM, POWER, C/C++11, and SC POPL Shaked FlurUniversity of Cambridge, Susmit SarkarUniversity of St. Andrews, UK, Christopher PulteUniversity of Cambridge, Kyndylan NienhuisUniversity of Cambridge, Luc MarangetINRIA Rocquencourt, Kathryn E. GrayUniversity of Cambridge, Ali SezginUniversity of Cambridge, Mark BattyUniversity of Kent, Peter SewellUniversity of Cambridge | ||
14:45 25mTalk | Dynamic Race Detection For C++11 POPL | ||
15:10 25mTalk | Serializability for Eventual Consistency: Criterion, Analysis and Applications POPL Lucas BrutschyETH Zurich, Dimitar DimitrovETH Zurich, Switzerland, Peter MüllerETH Zurich, Martin VechevETH Zurich Pre-print | ||
15:35 25mTalk | Thread Modularity at Many Levels: a Pearl in Compositional Verification POPL Jochen HoenickeUniversität Freiburg, Rupak MajumdarMPI-SWS, Andreas PodelskiUniversity of Freiburg, Germany | ||
14:20 - 16:00 | |||
14:20 25mTalk | Type Directed Compilation of Row-Typed Algebraic Effects POPL Daan LeijenMicrosoft Research | ||
14:45 25mTalk | Do be do be do POPL | ||
15:10 25mTalk | Dijkstra Monads for Free POPL Danel AhmanUniversity of Edinburgh, Cătălin HriţcuInria Paris, Kenji MaillardInria Paris, ENS Paris, and Microsoft Research, Guido MartínezCIFASIS-CONICET, Argentina, Gordon Plotkin, Jonathan ProtzenkoMicrosoft Research, Aseem RastogiMicrosoft Research India, Nikhil SwamyMicrosoft Research Pre-print | ||
15:35 25mTalk | Stateful Manifest Contracts POPL | ||
16:00 - 16:30 | |||
16:00 30mCoffee break | Break Catering | ||
16:30 - 17:20 | |||
16:30 25mTalk | A Semantic Account of Metric Preservation POPL Arthur Azevedo de AmorimUniversity of Pennsylvania, USA, Ikram CheriguiENS Paris, Marco GaboardiSUNY Buffalo, USA, Justin Hsu, Shin-ya KatsumataKyoto University | ||
16:55 25mTalk | Cantor Meets Scott: Semantic Foundations for Probabilistic Networks POPL Steffen SmolkaCornell University, Praveen KumarCornell University, Nate FosterCornell University, Dexter KozenCornell University, Alexandra SilvaUniversity College London DOI File Attached | ||
16:30 - 17:20 | |||
16:30 25mTalk | Genesis: Synthesizing Forwarding Tables in Multi-tenant Networks POPL Kausik SubramanianUniversity of Wisconsin-Madison, Loris D'AntoniUniversity of Wisconsin–Madison, Aditya AkellaUniversity of Wisconsin-Madison | ||
16:55 25mTalk | LOIS: syntax and semantics POPL | ||
17:20 - 18:20 | Business meetingPOPL at Auditorium Chair(s): Andrew D. GordonMicrosoft Research and University of Edinburgh | ||
17:20 20mTalk | PC Chair report POPL Andrew D. GordonMicrosoft Research and University of Edinburgh | ||
17:40 10mTalk | POPL 2018 presentation POPL | ||
17:50 30mMeeting | SIGPLAN business meeting POPL | ||
18:20 - 20:20 | Poster SessionStudent Research Competition at Auditorium Hall Chair(s): Qirun ZhangUniversity of California, Davis, Matteo CiminiIndiana University, USA, Julien SignolesCEA LIST, Kim NguyễnLRI, Université Paris-Sud | ||
18:20 10mDemonstration | Naturality despite Nontermination: A Logical Relation for Linear Types and Polymorphism Student Research Competition Nicholas RiouxNortheastern University | ||
18:30 10mDemonstration | Gradual Type Precision as Retraction Student Research Competition Max NewNortheastern University | ||
18:40 10mDemonstration | Linking Types: Specifying Safe Interoperability and Equivalences Student Research Competition Daniel PattersonNortheastern University | ||
18:50 10mDemonstration | A Monadic Framework for Bidirectional Programming Student Research Competition Li-yao XiaENS Paris | ||
19:00 10mDemonstration | Gradual Set-Theoretic Types Student Research Competition Victor LanvinENS Paris-Saclay | ||
19:10 10mDemonstration | Abstract Interpretation of High-Level Transformations Student Research Competition Ahmad Salim Al-SibahiIT University of Copenhagen, Denmark | ||
19:20 10mDemonstration | FairSquare: A Static Analysis Tool for Algorithmic Fairness Student Research Competition Samuel DrewsUniversity of Wisconsin-Madison | ||
19:30 10mDemonstration | Toward Type-Preserving Compilation of Coq Student Research Competition William J. BowmanNortheastern University | ||
19:40 10mDemonstration | A Symbolic Execution Framework for Haskell Student Research Competition Anton XueYale University | ||
19:50 10mDemonstration | Synthesizing Imperative Programs from Examples for Introductory Programming Assignments Student Research Competition Sunbeom SoKorea University | ||
20:00 10mDemonstration | Provenance for Configuration Language Security Student Research Competition Weili FuUniversity of Edinburgh | ||
20:10 10mDemonstration | A gradually typed polymorphic lambda calculus Student Research Competition Yuu IgarashiKyoto University | ||
Conference DayFri 20 JanDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
Conference Day
Fri 20 JanDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
09:00 - 09:05 | Student Competition AwardStudent Research Competition at Auditorium Chair(s): Kim NguyễnLRI, Université Paris-Sud | ||
09:00 5mAwards | Student Competition Award Student Research Competition | ||
09:05 - 10:00 | |||
09:05 55mTalk | Rust: from POPL to practice POPL Aaron TuronMPI-SWS | ||
10:00 - 10:30 | |||
10:00 30mCoffee break | Break Catering | ||
10:30 - 12:10 | |||
10:30 25mTalk | Component-Based Synthesis for Complex APIs POPL Yu FengUniversity of Texas at Austin, USA, Ruben Martins, Yuepeng WangUniversity of Texas at Austin, Isil DilligUT Austin, Thomas RepsUniversity of Wisconsin - Madison and Grammatech Inc. | ||
10:55 25mTalk | Learning nominal automata POPL Joshua MoermanRadboud University, Matteo SammartinoUniversity College London, Alexandra SilvaUniversity College London, Bartek KlinUniversity of Warsaw, Michał SzynwelskiUniversity of Warsaw | ||
11:20 25mTalk | On Verifying Causal Consistency POPL Ahmed BouajjaniIRIF, Université Paris Diderot, Constantin EneaLIAFA, Université Paris Diderot, Rachid Guerraoui, Jad HamzaLIAFA, Université Paris Diderot | ||
11:45 25mTalk | Complexity Verification Using Guided Theorem Enumeration POPL Akhilesh SrikanthGeorgia Institute of Technology, Burak SahinGeorgia Institute of Technology, William Harris | ||
10:30 - 12:10 | |||
10:30 25mTalk | Intersection Type Calculi of Bounded Dimension POPL | ||
10:55 25mTalk | Type Soundness Proofs with Definitional Interpreters POPL | ||
11:20 25mTalk | Computational Higher-Dimensional Type Theory POPL Carlo AngiuliCarnegie Mellon University, Robert Harper, Todd WilsonCalifornia State University Fresno | ||
11:45 25mTalk | Type Systems as Macros POPL Stephen ChangNortheastern University, Alex KnauthNortheastern University, Ben GreenmanNortheastern University | ||
12:10 - 14:20 | |||
12:10 2h10mLunch | Lunch Catering | ||
14:20 - 16:00 | |||
14:20 25mTalk | Parallel Functional Arrays POPL | ||
14:45 25mTalk | A Short Counterexample Property for Safety and Liveness Verification of Fault-tolerant Distributed Algorithms POPL DOI Pre-print | ||
15:10 25mTalk | Analyzing divergence in bisimulation semantics POPL Xinxin LiuInstitute of software, Chinese academy of sciences, Tingting Yu, Wenhui ZhangInstitute of software, Chinese academy of sciences | ||
15:35 25mTalk | Fencing off Go: Liveness and Safety for Channel-Based Programming POPL Julien LangeImperial College London, Nicholas NgImperial College London, Bernardo ToninhoImperial College London, Nobuko YoshidaImperial College London, UK Pre-print | ||
14:20 - 16:00 | Gradual Typing and ContractsPOPL at Auditorium Chair(s): Ronald GarciaUniversity of British Columbia | ||
14:20 25mTalk | Big Types in Little Runtime: Open World Soundness and Collaborative Blame for Gradual Type System POPL | ||
14:45 25mTalk | Gradual Refinement Types POPL Link to publication DOI Pre-print | ||
15:10 25mTalk | Automatically Generating the Dynamic Semantics of Gradually Typed Languages POPL | ||
15:35 25mTalk | Sums of Uncertainty: Refinements go gradual POPL | ||
16:00 - 16:30 | |||
16:00 30mCoffee break | Break Catering | ||
16:30 - 17:45 | |||
16:30 25mTalk | Invariants of Quantum Programs: Characterisations and Generation POPL Mingsheng YingUniversity of Technology Sydney, Australia, Shenggang YingUniversity of Technology Sydney, Australia, Xiaodi WuUniversity of Oregon, USA | ||
16:55 25mTalk | The Geometry of Parallelism. Classical, Probabilistic, and Quantum Effects POPL Ugo Dal LagoUniversity of Bologna, France, Claudia Faggian, Benoit ValironLRI, CentraleSupelec, Univ. Paris Saclay, Akira YoshimizuUniv.Tokyo | ||
17:20 25mTalk | QWIRE: A Core Language for Quantum Circuits POPL | ||
16:30 - 17:45 | |||
16:30 25mTalk | LMS-Verify: Abstraction Without Regret for Verified Systems Programming POPL | ||
16:55 25mTalk | Hypercollecting Semantics and its Application to Static Analysis of Information Flow POPL Mounir AssafStevens Institute of Technology, David NaumannStevens Institute of Technology, Julien SignolesCEA LIST, Éric TotelCentraleSupélec, Frédéric TronelCentraleSupélec | ||
17:20 25mTalk | LightDP: Towards Automating Differential Privacy Proofs POPL Danfeng ZhangPennsylvania State University, Daniel KiferDept. of Computer Science and Engineering, Penn State University | ||
Conference DaySat 21 JanDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
Conference Day
Sat 21 JanDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
08:45 - 09:00 | |||
08:45 15mDay opening | Opening N40AI | ||
08:55 - 09:00 | |||
08:55 5mTalk | Welcome PiP | ||
09:00 - 10:00 | |||
09:00 30mTalk | Abstract Interpretation in Absint N40AI Christian FerdinandAbsInt | ||
09:30 30mTalk | Abstract Interpretation in Facebook N40AI Francesco LogozzoFacebook | ||
09:00 - 10:00 | |||
09:00 60mTalk | Invited Talk -- Demonstration of the Iris separation logic in Coq CoqPL | ||
09:00 - 10:00 | |||
09:00 30mTalk | Andrew Kennedy (Facebook) Static type checking for PHP PiP | ||
09:30 30mTalk | Jean-Louis Colaco (Ansys - Esterel Technologies) A brief history of the Scade language PiP | ||
09:00 - 10:00 | |||
09:00 15mTalk | Welcome RDP | ||
09:15 45mTalk | Automatic Verification of Database-Centric Workflows RDP | ||
09:00 - 10:00 | |||
09:00 60mTalk | Keynote talk: Reasoning about Functional Programs: Exploring, Testing and Inductive Proofs. Off the Beaten Track Moa JohanssonChalmers University of Technology | ||
10:00 - 10:30 | |||
10:00 30mCoffee break | Break Catering | ||
10:30 - 12:00 | |||
10:30 30mTalk | Abstract Interpretation in Amazon N40AI Byron CookAmazon | ||
11:00 30mTalk | Abstract Interpretation at Galois N40AI Aaron TombGalois, Inc. | ||
11:30 30mTalk | Systems biology N40AI Vincent DanosENS Paris/CNRS | ||
10:30 - 12:10 | |||
10:30 25mTalk | IxFree: Step-Indexed Logical Relations in Coq CoqPL File Attached | ||
10:55 25mTalk | Logical Relations in Iris CoqPL Amin Timanyimec - Distrinet, KU Leuven, Robbert KrebbersDelft University of Technology, Netherlands, Lars BirkedalAarhus University File Attached | ||
11:20 25mTalk | Predicate Monads: A Framework for Proving Generic Properties of Monadic Programs via Rewriting CoqPL File Attached | ||
11:45 25mTalk | ppsimpl: a reflexive Coq tactic for canonising goals CoqPL File Attached | ||
10:30 - 12:00 | |||
10:30 30mTalk | Verification Challenges in Applications of Blockchain for Business Collaboration RDP Takaaki TateishiIBM Research - Tokyo | ||
11:00 30mTalk | Fiat: A New Take on Domain-Specific Languages by Programming with Specifications RDP | ||
11:30 30mTalk | Parallel-Correctness and Transferability for Conjunctive Queries RDP | ||
10:30 - 12:10 | |||
10:30 25mTalk | Can we machine-learn programming language semantics? Off the Beaten Track File Attached | ||
10:55 25mTalk | How Far Apart Should Those Programs Be? Off the Beaten Track Ugo Dal LagoUniversity of Bologna, France File Attached | ||
11:20 25mTalk | Programming Quantum Annealers Off the Beaten Track File Attached | ||
11:45 25mTalk | Understanding the POSIX Shell as a Programming Language Off the Beaten Track Michael GreenbergPomona College File Attached | ||
12:00 - 14:00 | |||
12:00 2hLunch | Lunch Catering | ||
14:00 - 15:30 | Security, Big Code and Synthesis N40AI at Amphitheater 44 Chair(s): Xavier RivalINRIA/CNRS/ENS Paris | ||
14:00 30mTalk | Security N40AI Michael HicksUniversity of Maryland at College Park, USA | ||
14:30 30mTalk | Big Code N40AI Bor-Yuh Evan ChangUniversity of Colorado Boulder | ||
15:00 30mTalk | Program synthesis N40AI Eran YahavTechnion | ||
14:00 - 15:30 | |||
14:00 60mTalk | Invited Talk -- Managing Logical and Computational Complexity using Program Transformations CoqPL | ||
15:00 30mDemonstration | Session with the Coq Development Team CoqPL Matthieu SozeauInria | ||
14:00 - 15:30 | |||
14:00 30mTalk | John Hughes (Quviq/Chalmers) Properties in practice: lessons from ten years of QuickCheck PiP | ||
14:30 30mTalk | Byron Cook (Amazon) Automated Reasoning about AWS PiP | ||
15:00 30mTalk | Steve Zdancewic (U.Penn) Vellvm2: Semantics and Verification for LLVM PiP | ||
14:00 - 15:30 | |||
14:00 45mTalk | Synthesizing Data-parallel Programs RDP Aws AlbarghouthiUniversity of Wisconsin - Madison | ||
14:45 45mTalk | Cosette: A Solver for SQL Equivalences RDP Alvin CheungUniversity of Washington | ||
14:00 - 15:25 | |||
14:00 60mTalk | Keynote talk: Varieties of Programming Experience Off the Beaten Track Alan BlackwellUniversity of Cambridge | ||
15:00 25mTalk | Bootstrapping the next generation of mathematical social machines Off the Beaten Track File Attached | ||
15:30 - 16:00 | |||
15:30 30mCoffee break | Break Catering | ||
16:00 - 18:30 | System Verification and Patrick Cousot's KeynoteN40AI at Amphitheater 44 Chair(s): Francesco RanzatoUniversity of Padova | ||
16:00 30mTalk | System verification N40AI Arie GurfinkelUniversity of Waterloo | ||
16:30 75mTalk | Keynote: the Next 40 years of Abstract Interpretation N40AI Patrick CousotNew York University | ||
17:45 45mSocial Event | Concrete Cheese and Wine N40AI | ||
16:00 - 18:00 | |||
16:00 30mTalk | Christopher Pulte/Kathryn Gray (Cambridge) REMS machine models PiP | ||
16:30 60mTalk | Discussion: Methods and Tools for large-scale semantics PiP | ||
16:00 - 18:00 | |||
16:00 30mTalk | Building performance-sensitive systems in high-level languages RDP | ||
16:30 30mTalk | Programming Language Ideas Escape the Lab: Declarative Data Description Languages for Managing Ad hoc Data RDP Kathleen FisherTufts University | ||
17:00 30mTalk | Computation with Atoms RDP | ||
17:30 30mTalk | Discussion RDP | ||
16:00 - 18:05 | |||
16:00 25mTalk | Designing extensible, domain-specific languages for mathematical diagrams Off the Beaten Track Katherine Ye, Keenan Crane, Jonathan AldrichCarnegie Mellon University, Joshua SunshineCarnegie Mellon University File Attached | ||
16:25 25mTalk | Laziness Boxes You In Off the Beaten Track File Attached | ||
16:50 25mTalk | Programming with Epistemic Logic Off the Beaten Track File Attached | ||
17:15 25mTalk | Preventing False Discoveries in Adaptive Data Analysis: a Programming Language approach Off the Beaten Track Marco GaboardiSUNY Buffalo, USA File Attached | ||
17:40 25mTalk | Running Incomplete Programs Off the Beaten Track Ian VoyseyCarnegie Mellon University, Cyrus OmarCarnegie Mellon University, Matthew HammerUniversity of Colorado, Boulder File Attached | ||
19:00 - 21:00 | |||
19:00 2hSocial Event | CoqPL Social Event CoqPL | ||