{"id":558255,"date":"2019-01-03T13:11:54","date_gmt":"2019-01-03T21:11:54","guid":{"rendered":"https:\/\/www.microsoft.com\/en-us\/research\/?post_type=msr-event&p=558255"},"modified":"2025-08-06T11:56:40","modified_gmt":"2025-08-06T18:56:40","slug":"popl-2019","status":"publish","type":"msr-event","link":"https:\/\/www.microsoft.com\/en-us\/research\/event\/popl-2019\/","title":{"rendered":"Microsoft @ POPL 2019"},"content":{"rendered":"\n\n

Venue: <\/strong>Hotel Cascais Miragem (opens in new tab)<\/span><\/a>
\nAv.Marginal n.8554
\n2754-536
\nCascais\/Lisbon
\nPortugal<\/p>\n

Website:<\/strong> POPL 2019 (opens in new tab)<\/span><\/a>Opens in a new tab<\/span><\/p>\n

Microsoft is excited to be a Platinum sponsor of the 46th ACM SIGPLAN Symposium on Principles of Programming Languages (opens in new tab)<\/span><\/a>. Stop by our booth to learn about our latest research and find out about career opportunities with Microsoft.<\/p>\n

Microsoft Attendees<\/h3>\n

Tom Ball<\/a>
\nAntoine Delignat-Lavaud<\/a>
\nChris Hawblitzel<\/a>
\nNuno Lopes<\/a>
\nJonathan Protzenko<\/a>
\nTahina Ramananandro<\/a>
\nAndrey Rybalchenko<\/a>
\nSantiago Zanella-Beguelin<\/a>
\nAndy Gordon<\/a>
\nNikhil Swamy<\/a><\/p>\n

Research Paper Committee<\/h3>\n

Dimitrios Vytiniotis (opens in new tab)<\/span><\/a>, Matthew Parkinson<\/a>, Nikhil Swamy (opens in new tab)<\/span><\/a><\/p>\n

Artifact Evaluation Committee<\/h3>\n

Jonathan Protzenko<\/a><\/p>\n

Steering Committee<\/h3>\n

Andrew D. Gordon<\/a><\/p>\n

Co-Located Conferences<\/h3>\n

Certified Programs and Proofs (CPP)<\/h4>\n

Chris Hawblitzel<\/a><\/p>\n

Principles of Secure Compilation(PriSC)<\/h4>\n

C\u00e9dric Fournet (opens in new tab)<\/span><\/a><\/p>\n

Invited Speakers<\/h3>\n

VMCAI 2019, co-located
\nTuesday, January 15, 2019 | 9:00 AM\u201310:30 AM
\nSemantics for Compiler IRs: Undefined Behavior is not Evil!<\/strong> (opens in new tab)<\/span><\/a>
\nNuno Lopes<\/a><\/p>\n

Opens in a new tab<\/span><\/p>\n

Wednesday, January 16, 2019 | 1:45 PM\u20132:07 PM | Probabilistic Programming and Semantics
\nProbabilistic Programming with Densities in SlicStan: Efficient, Flexible and Deterministic (opens in new tab)<\/span><\/a><\/h4>\n

Maria I. Gorinova (opens in new tab)<\/span><\/a>, Andrew D. Gordon<\/a>, Charles Sutton (opens in new tab)<\/span><\/a><\/p>\n

Friday, January 18, 2019 | 5:21 PM\u20135:43 PM | Verified Compilation and Concurrency
\nA Verified, Efficient Embedding of a Verifiable Assembly Language<\/a><\/h4>\n

Aymeric Fromherz, Nick Giannarakis, Chris Hawblitzel<\/a>, Bryan Parno, Aseem Rastogi<\/a>, Nikhil Swamy (opens in new tab)<\/span><\/a><\/p>\n

Co-Located Conferences<\/h3>\n

Tuesday, January 15, 2019 | 4:30 PM\u20135:00 PM | Networks and Concurrency at VMCAI
\nFast BGP Simulation of Large Datacenters (opens in new tab)<\/span><\/a><\/h4>\n

Nuno Lopes<\/a>, Andrey Rybalchenko<\/a><\/p>\n

Opens in a new tab<\/span><\/p>\n

Open Source Tools for System Correctness<\/h4>\n

Automata:<\/strong> Automata (opens in new tab)<\/span><\/a> is a .NET library that provides algorithms for composing and analyzing regular expressions, automata, and transducers. In addition to classical word automata, it also includes algorithms for analysis of tree automata and tree transducers. The library covers algorithms over finite alphabets as well as their symbolic counterparts. Predicates can be supported by an SMT solver as a plugin.<\/p>\n

Corral Program Verifier:<\/strong>\u00a0Corral (opens in new tab)<\/span><\/a> is a whole-program analysis tool for\u00a0Boogie (opens in new tab)<\/span><\/a>\u00a0programs. Corral uses goal-directed symbolic search techniques to find assertion violations.\u00a0It leverages the automated\u00a0theorem prover Z3. Corral, by default, does a bounded search up to a recursion depth and fixed number of context switches. Corral also supports the\u00a0Duality (opens in new tab)<\/span><\/a>\u00a0extension for constructing\u00a0inductive proofs of correctness of programs.<\/p>\n

Ivy:<\/strong> IVy (opens in new tab)<\/span><\/a> is a tool intended to allow interactive development of protocols and their proofs of correctness and to provide a platform for developing and experimenting with automated proof techniques. In particular, IVy provides interactive visualization of automated proofs, and supports a use model in which the human protocol designer and the automated tool interact to expose errors and prove correctness.<\/p>\n

Lean Theorem Prover:<\/strong> Lean (opens in new tab)<\/span><\/a> is an open source theorem prover and programming language. Lean aims to bridge the gap between interactive and automated theorem proving, by situating automated tools and methods in a framework that supports user interaction and the construction of fully specified axiomatic proofs.<\/p>\n

P\/P#:<\/strong> P\/P# (opens in new tab)<\/span><\/a> are languages for asynchronous event-driven programming that allow the programmer to specify the system as a collection of interacting state machines, which communicate with each other using events. P\/P# unifies modeling and programming into one activity for the programmer. Not only can a P\/P# program be compiled into executable code, but it can also be validated using systematic testing.<\/p>\n

Project Everest:<\/strong> Everest (opens in new tab)<\/span><\/a> is the combination of the following projects, that together are used to prove correct\/secure and generate a C library that efficiently implements TLS 1.3<\/p>\n