{"id":628671,"date":"2020-01-14T08:57:16","date_gmt":"2020-01-14T16:57:16","guid":{"rendered":"https:\/\/www.microsoft.com\/en-us\/research\/?post_type=msr-event&#038;p=628671"},"modified":"2025-08-06T11:53:34","modified_gmt":"2025-08-06T18:53:34","slug":"popl-2020","status":"publish","type":"msr-event","link":"https:\/\/www.microsoft.com\/en-us\/research\/event\/popl-2020\/","title":{"rendered":"Microsoft @ POPL 2020"},"content":{"rendered":"\n\n<p><strong>Venue:<\/strong> JW Marriott New Orleans<br \/>\n614 Canal St<br \/>\nNew Orleans, Louisiana<\/p>\n<p><strong>Website:<\/strong> <a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" href=\"https:\/\/popl20.sigplan.org\/\" target=\"_blank\" rel=\"noopener noreferrer\">POPL 2020<span class=\"sr-only\"> (opens in new tab)<\/span><\/a><\/p>\n<p><strong>Contact us:<\/strong> <a href=\"mailto:msrevent@microsoft.com\">msrevent@microsoft.com<\/a><span id=\"label-external-link\" class=\"sr-only\" aria-hidden=\"true\">Opens in a new tab<\/span><\/p>\n<p>The annual Symposium on Principles of Programming Languages is a forum for the discussion of all aspects of programming languages and programming systems. Both theoretical and experimental papers are welcome, on topics ranging from formal frameworks to experience reports. We seek submissions that make principled, enduring contributions to the theory, design, understanding, implementation or application of programming languages.<\/p>\n<h3>Research Papers Program Committee Members<\/h3>\n<ul>\n<li><a href=\"https:\/\/www.microsoft.com\/en-us\/research\/people\/fournet\/\">C\u00e9dric Fournet<\/a><\/li>\n<li><a href=\"https:\/\/www.microsoft.com\/en-us\/research\/people\/margus\/\">Margus Veanes<\/a><\/li>\n<li><a href=\"https:\/\/www.microsoft.com\/en-us\/research\/people\/shuvendu\/\">Shuvendu K. Lahiri<\/a><\/li>\n<\/ul>\n<p><span id=\"label-external-link\" class=\"sr-only\" aria-hidden=\"true\">Opens in a new tab<\/span><\/p>\n<h2>Microsoft main conference presentation schedule<\/h2>\n<h3>Sunday, January 19<\/h3>\n<p>Programming Languages for Quantum Computing (PLanQC) | Workshop<br \/>\nProgram Committee Members: <a href=\"https:\/\/www.microsoft.com\/en-us\/research\/people\/chgranad\/\">Chris Granade<\/a>, <a href=\"https:\/\/www.microsoft.com\/en-us\/research\/people\/beheim\/\">Bettina Heim<\/a><br \/>\n10:30 AM\u201311:00 AM, Invited talk: <a href=\"https:\/\/www.microsoft.com\/en-us\/research\/people\/beheim\/\">Bettina Heim<\/a><\/p>\n<h3>Monday, January 20<\/h3>\n<p>Partial Evaluation and Program Manipulation (PEPM) | Workshop<br \/>\n11:25 AM\u201312:00 PM, Panelist: <a href=\"https:\/\/www.microsoft.com\/en-us\/research\/people\/nbjorner\/\">Nikolaj Bj\u00f8rner<\/a><\/p>\n<h3>Tuesday, January 21<\/h3>\n<p><strong>HASE 2020 Workshop on High Assurance Systems Engineering<\/strong> | Workshop<br \/>\nCo-organizer: <a href=\"https:\/\/www.microsoft.com\/en-us\/research\/people\/protz\/\">Jonathan Protzenko<\/a><\/p>\n<p><strong>Languages for Inference (LAFI)<\/strong> | Workshop<br \/>\nSteering Committee Member: <a href=\"https:\/\/www.microsoft.com\/en-us\/research\/people\/adg\/\">Andrew Gordon<\/a><\/p>\n<p><strong>Programming Languages Mentoring Workshop (PLMW)<\/strong> | Workshop<br \/>\n2:00 PM\u20133:05 PM, Panelist: <a href=\"https:\/\/www.microsoft.com\/en-us\/research\/people\/jufranc\/\">Juliana Franco<\/a><\/p>\n<h3>Thursday, January 23<\/h3>\n<p>Research Papers \u2013 Abstract Interpretation<br \/>\n2:21 PM\u20132:43 PM<br \/>\n<strong>Abstract Interpretation of Distributed Network Control Planes<\/strong><br \/>\n<a href=\"https:\/\/www.microsoft.com\/en-us\/research\/people\/rybecket\/\">Ryan Beckett<\/a>, Aarti Gupta, Ratul Mahajan, David Walker<\/p>\n<h3>Saturday, January 25<\/h3>\n<p><strong>Principles of Secure Compilation (PriSC)<\/strong> | Workshop<br \/>\nProgram Committee Member, Session Chair: <a href=\"https:\/\/www.microsoft.com\/en-us\/research\/people\/protz\/\">Jonathan Protzenko<\/a><\/p>\n<h2>Co-located conferences<\/h2>\n<h3>Monday, January 20<\/h3>\n<p><strong>22nd Symposium on Practical Aspects of Declarative Languages (PADL 2020)<\/strong><br \/>\n8:45 AM\u20139:35 AM, Invited Talk: <a href=\"https:\/\/www.microsoft.com\/en-us\/research\/people\/nbjorner\/\">Nikolaj Bj\u00f8rner<\/a><br \/>\n11:25 AM\u201312:00 PM, Panelist: <a href=\"https:\/\/www.microsoft.com\/en-us\/research\/people\/nbjorner\/\">Nikolaj Bj\u00f8rner<\/a><\/p>\n<h3>Tuesday, January 21<\/h3>\n<p>12:00 PM\u201312:30 PM | Talk<br \/>\n<strong>Solving LIA* Using Approximations<\/strong><br \/>\nMaxwell Levatich, <a href=\"https:\/\/www.microsoft.com\/en-us\/research\/people\/nbjorner\/\">Nikolaj Bj\u00f8rner<\/a>, Ruzica Piskac, Sharon Shoham<span id=\"label-external-link\" class=\"sr-only\" aria-hidden=\"true\">Opens in a new tab<\/span><\/p>\n<ul>\n<li>Automata: <a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" href=\"http:\/\/github.com\/AutomataDotNet\/Automata\" target=\"_blank\" rel=\"noopener\">github.com\/AutomataDotNet\/Automata<span class=\"sr-only\"> (opens in new tab)<\/span><\/a><\/li>\n<li>Ivy: <a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" href=\"http:\/\/github.com\/Microsoft\/ivy\" target=\"_blank\" rel=\"noopener\">github.com\/Microsoft\/ivy<span class=\"sr-only\"> (opens in new tab)<\/span><\/a><\/li>\n<li>Lean Theorem Prover: <a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" href=\"http:\/\/leanprover.github.io\" target=\"_blank\" rel=\"noopener\">leanprover.github.io<span class=\"sr-only\"> (opens in new tab)<\/span><\/a><\/li>\n<li>Network Verification: <a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" href=\"http:\/\/github.com\/Z3Prover\/\" target=\"_blank\" rel=\"noopener\">github.com\/Z3Prover\/FirewallChecker<span class=\"sr-only\"> (opens in new tab)<\/span><\/a><\/li>\n<li>P\/P#: <a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" href=\"http:\/\/github.com\/p-org\" target=\"_blank\" rel=\"noopener\">github.com\/p-org<span class=\"sr-only\"> (opens in new tab)<\/span><\/a><\/li>\n<li>Project Everest: <a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" href=\"http:\/\/project-everest.github.io\" target=\"_blank\" rel=\"noopener\">project-everest.github.io<span class=\"sr-only\"> (opens in new tab)<\/span><\/a>\n<ul>\n<li>F*: <a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" href=\"http:\/\/fstar-lang.org\" target=\"_blank\" rel=\"noopener\">fstar-lang.org<span class=\"sr-only\"> (opens in new tab)<\/span><\/a><\/li>\n<li>miTLS: <a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" href=\"http:\/\/mitls.org\" target=\"_blank\" rel=\"noopener\">mitls.org<span class=\"sr-only\"> (opens in new tab)<\/span><\/a><\/li>\n<li>KreMLin: <a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" href=\"http:\/\/github.com\/FStarLang\/kremlin\" target=\"_blank\" rel=\"noopener\">github.com\/FStarLang\/kremlin<span class=\"sr-only\"> (opens in new tab)<\/span><\/a><\/li>\n<li>HACL*: <a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" href=\"http:\/\/github.com\/project-everest\/hacl-star\" target=\"_blank\" rel=\"noopener\">github.com\/project-everest\/hacl-star<span class=\"sr-only\"> (opens in new tab)<\/span><\/a><\/li>\n<li>Vale: <a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" href=\"http:\/\/github.com\/project-everest\/vale\" target=\"_blank\" rel=\"noopener\">github.com\/project-everest\/vale<span class=\"sr-only\"> (opens in new tab)<\/span><\/a><\/li>\n<\/ul>\n<\/li>\n<li>Q#: <a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" href=\"https:\/\/github.com\/Microsoft\/qsharp-compiler\" target=\"_blank\" rel=\"noopener\">github.com\/Microsoft\/qsharp-compiler<span class=\"sr-only\"> (opens in new tab)<\/span><\/a><\/li>\n<li>TLA+: <a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" href=\"http:\/\/github.com\/tlaplus\/tlaplus\" target=\"_blank\" rel=\"noopener\">github.com\/tlaplus\/tlaplus<span class=\"sr-only\"> (opens in new tab)<\/span><\/a><\/li>\n<li>VeriSol: <a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" href=\"https:\/\/github.com\/Microsoft\/verisol\" target=\"_blank\" rel=\"noopener\">github.com\/Microsoft\/verisol<span class=\"sr-only\"> (opens in new tab)<\/span><\/a><\/li>\n<li>Z3 Theorem Prover: <a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" href=\"http:\/\/github.com\/Z3Prover\/z3\" target=\"_blank\" rel=\"noopener\">github.com\/Z3Prover\/z3<span class=\"sr-only\"> (opens in new tab)<\/span><\/a><\/li>\n<\/ul>\n<p><span id=\"label-external-link\" class=\"sr-only\" aria-hidden=\"true\">Opens in a new tab<\/span><\/p>\n<p>Job openings are always searchable at <a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" href=\"https:\/\/careers.microsoft.com\/us\/en\" target=\"_blank\" rel=\"noopener\">https:\/\/careers.microsoft.com\/<span class=\"sr-only\"> (opens in new tab)<\/span><\/a> including:<\/p>\n<ul>\n<li><a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" href=\"https:\/\/careers.microsoft.com\/professionals\/us\/en\/search-results?keywords=compiler\" target=\"_blank\" rel=\"noopener\">Compiler Jobs<span class=\"sr-only\"> (opens in new tab)<\/span><\/a><\/li>\n<li><a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" href=\"https:\/\/careers.microsoft.com\/professionals\/us\/en\/search-results?keywords=runtime\" target=\"_blank\" rel=\"noopener\">Runtime Jobs<span class=\"sr-only\"> (opens in new tab)<\/span><\/a><\/li>\n<li><a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" href=\"https:\/\/careers.microsoft.com\/professionals\/us\/en\/search-results?keywords=visual%20studio\" target=\"_blank\" rel=\"noopener\">Openings in Visual Studio<span class=\"sr-only\"> (opens in new tab)<\/span><\/a><\/li>\n<li><a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" href=\"https:\/\/careers.microsoft.com\/us\/en\/job\/740235\/Principal-Software-Engineering-Manager\" target=\"_blank\" rel=\"noopener\">Visual C++ Principal Software Engineering Manager<span class=\"sr-only\"> (opens in new tab)<\/span><\/a><\/li>\n<li><a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" href=\"https:\/\/careers.microsoft.com\/us\/en\/job\/725691\/Program-Manager-2\" target=\"_blank\" rel=\"noopener\">Visual C++ Program Manager 2<span class=\"sr-only\"> (opens in new tab)<\/span><\/a><\/li>\n<\/ul>\n<p><span id=\"label-external-link\" class=\"sr-only\" aria-hidden=\"true\">Opens in a new tab<\/span><\/p>\n","protected":false},"excerpt":{"rendered":"<p>The annual Symposium on Principles of Programming Languages is a forum for the discussion of all aspects of programming languages and programming systems. Both theoretical and experimental papers are welcome, on topics ranging from formal frameworks to experience reports. We seek submissions that make principled, enduring contributions to the theory, design, understanding, implementation or application of programming languages.<\/p>\n","protected":false},"featured_media":571890,"template":"","meta":{"msr-url-field":"","msr-podcast-episode":"","msrModifiedDate":"","msrModifiedDateEnabled":false,"ep_exclude_from_search":false,"_classifai_error":"","msr_startdate":"2020-01-19","msr_enddate":"2020-01-25","msr_location":"New Orleans, Louisiana","msr_expirationdate":"","msr_event_recording_link":"","msr_event_link":"","msr_event_link_redirect":false,"msr_event_time":"","msr_hide_region":false,"msr_private_event":false,"msr_hide_image_in_river":0,"footnotes":""},"research-area":[13560],"msr-region":[197900],"msr-event-type":[197941],"msr-video-type":[],"msr-locale":[268875],"msr-program-audience":[],"msr-post-option":[],"msr-impact-theme":[],"class_list":["post-628671","msr-event","type-msr-event","status-publish","has-post-thumbnail","hentry","msr-research-area-programming-languages-software-engineering","msr-region-north-america","msr-event-type-conferences","msr-locale-en_us"],"msr_about":"<!-- wp:msr\/event-details {\"title\":\"Microsoft @ POPL 2020\",\"backgroundColor\":\"grey\",\"image\":{\"id\":571890,\"url\":\"https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2019\/03\/iclr2019_1920x720.jpg\",\"alt\":\"\"}} \/-->\n\n<!-- wp:msr\/content-tabs --><!-- wp:msr\/content-tab {\"title\":\"About\"} --><!-- wp:freeform --><p><strong>Venue:<\/strong> JW Marriott New Orleans<br \/>\n614 Canal St<br \/>\nNew Orleans, Louisiana<\/p>\n<p><strong>Website:<\/strong> <a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" href=\"https:\/\/popl20.sigplan.org\/\" target=\"_blank\" rel=\"noopener noreferrer\">POPL 2020<\/a><\/p>\n<p><strong>Contact us:<\/strong> <a href=\"mailto:msrevent@microsoft.com\">msrevent@microsoft.com<\/a><span id=\"label-external-link\" class=\"sr-only\" aria-hidden=\"true\">Opens in a new tab<\/span><\/p>\n<p>The annual Symposium on Principles of Programming Languages is a forum for the discussion of all aspects of programming languages and programming systems. Both theoretical and experimental papers are welcome, on topics ranging from formal frameworks to experience reports. We seek submissions that make principled, enduring contributions to the theory, design, understanding, implementation or application of programming languages.<\/p>\n<h3>Research Papers Program Committee Members<\/h3>\n<ul>\n<li><a href=\"https:\/\/www.microsoft.com\/en-us\/research\/people\/fournet\/\">C\u00e9dric Fournet<\/a><\/li>\n<li><a href=\"https:\/\/www.microsoft.com\/en-us\/research\/people\/margus\/\">Margus Veanes<\/a><\/li>\n<li><a href=\"https:\/\/www.microsoft.com\/en-us\/research\/people\/shuvendu\/\">Shuvendu K. Lahiri<\/a><\/li>\n<\/ul>\n<p><span id=\"label-external-link\" class=\"sr-only\" aria-hidden=\"true\">Opens in a new tab<\/span><\/p>\n<!-- \/wp:freeform --><!-- \/wp:msr\/content-tab --><!-- wp:msr\/content-tab {\"title\":\"Sessions\"} --><!-- wp:freeform --><h2>Microsoft main conference presentation schedule<\/h2>\n<h3>Sunday, January 19<\/h3>\n<p>Programming Languages for Quantum Computing (PLanQC) | Workshop<br \/>\nProgram Committee Members: <a href=\"https:\/\/www.microsoft.com\/en-us\/research\/people\/chgranad\/\">Chris Granade<\/a>, <a href=\"https:\/\/www.microsoft.com\/en-us\/research\/people\/beheim\/\">Bettina Heim<\/a><br \/>\n10:30 AM\u201311:00 AM, Invited talk: <a href=\"https:\/\/www.microsoft.com\/en-us\/research\/people\/beheim\/\">Bettina Heim<\/a><\/p>\n<h3>Monday, January 20<\/h3>\n<p>Partial Evaluation and Program Manipulation (PEPM) | Workshop<br \/>\n11:25 AM\u201312:00 PM, Panelist: <a href=\"https:\/\/www.microsoft.com\/en-us\/research\/people\/nbjorner\/\">Nikolaj Bj\u00f8rner<\/a><\/p>\n<h3>Tuesday, January 21<\/h3>\n<p><strong>HASE 2020 Workshop on High Assurance Systems Engineering<\/strong> | Workshop<br \/>\nCo-organizer: <a href=\"https:\/\/www.microsoft.com\/en-us\/research\/people\/protz\/\">Jonathan Protzenko<\/a><\/p>\n<p><strong>Languages for Inference (LAFI)<\/strong> | Workshop<br \/>\nSteering Committee Member: <a href=\"https:\/\/www.microsoft.com\/en-us\/research\/people\/adg\/\">Andrew Gordon<\/a><\/p>\n<p><strong>Programming Languages Mentoring Workshop (PLMW)<\/strong> | Workshop<br \/>\n2:00 PM\u20133:05 PM, Panelist: <a href=\"https:\/\/www.microsoft.com\/en-us\/research\/people\/jufranc\/\">Juliana Franco<\/a><\/p>\n<h3>Thursday, January 23<\/h3>\n<p>Research Papers \u2013 Abstract Interpretation<br \/>\n2:21 PM\u20132:43 PM<br \/>\n<strong>Abstract Interpretation of Distributed Network Control Planes<\/strong><br \/>\n<a href=\"https:\/\/www.microsoft.com\/en-us\/research\/people\/rybecket\/\">Ryan Beckett<\/a>, Aarti Gupta, Ratul Mahajan, David Walker<\/p>\n<h3>Saturday, January 25<\/h3>\n<p><strong>Principles of Secure Compilation (PriSC)<\/strong> | Workshop<br \/>\nProgram Committee Member, Session Chair: <a href=\"https:\/\/www.microsoft.com\/en-us\/research\/people\/protz\/\">Jonathan Protzenko<\/a><\/p>\n<h2>Co-located conferences<\/h2>\n<h3>Monday, January 20<\/h3>\n<p><strong>22nd Symposium on Practical Aspects of Declarative Languages (PADL 2020)<\/strong><br \/>\n8:45 AM\u20139:35 AM, Invited Talk: <a href=\"https:\/\/www.microsoft.com\/en-us\/research\/people\/nbjorner\/\">Nikolaj Bj\u00f8rner<\/a><br \/>\n11:25 AM\u201312:00 PM, Panelist: <a href=\"https:\/\/www.microsoft.com\/en-us\/research\/people\/nbjorner\/\">Nikolaj Bj\u00f8rner<\/a><\/p>\n<h3>Tuesday, January 21<\/h3>\n<p>12:00 PM\u201312:30 PM | Talk<br \/>\n<strong>Solving LIA* Using Approximations<\/strong><br \/>\nMaxwell Levatich, <a href=\"https:\/\/www.microsoft.com\/en-us\/research\/people\/nbjorner\/\">Nikolaj Bj\u00f8rner<\/a>, Ruzica Piskac, Sharon Shoham<span id=\"label-external-link\" class=\"sr-only\" aria-hidden=\"true\">Opens in a new tab<\/span><\/p>\n<!-- \/wp:freeform --><!-- \/wp:msr\/content-tab --><!-- wp:msr\/content-tab {\"title\":\"Open source tools\"} --><!-- wp:freeform --><ul>\n<li>Automata: <a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" href=\"http:\/\/github.com\/AutomataDotNet\/Automata\" target=\"_blank\" rel=\"noopener\">github.com\/AutomataDotNet\/Automata<span class=\"sr-only\"> (opens in new tab)<\/span><\/a><\/li>\n<li>Ivy: <a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" href=\"http:\/\/github.com\/Microsoft\/ivy\" target=\"_blank\" rel=\"noopener\">github.com\/Microsoft\/ivy<span class=\"sr-only\"> (opens in new tab)<\/span><\/a><\/li>\n<li>Lean Theorem Prover: <a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" href=\"http:\/\/leanprover.github.io\" target=\"_blank\" rel=\"noopener\">leanprover.github.io<span class=\"sr-only\"> (opens in new tab)<\/span><\/a><\/li>\n<li>Network Verification: <a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" href=\"http:\/\/github.com\/Z3Prover\/\" target=\"_blank\" rel=\"noopener\">github.com\/Z3Prover\/FirewallChecker<span class=\"sr-only\"> (opens in new tab)<\/span><\/a><\/li>\n<li>P\/P#: <a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" href=\"http:\/\/github.com\/p-org\" target=\"_blank\" rel=\"noopener\">github.com\/p-org<span class=\"sr-only\"> (opens in new tab)<\/span><\/a><\/li>\n<li>Project Everest: <a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" href=\"http:\/\/project-everest.github.io\" target=\"_blank\" rel=\"noopener\">project-everest.github.io<span class=\"sr-only\"> (opens in new tab)<\/span><\/a>\n<ul>\n<li>F*: <a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" href=\"http:\/\/fstar-lang.org\" target=\"_blank\" rel=\"noopener\">fstar-lang.org<span class=\"sr-only\"> (opens in new tab)<\/span><\/a><\/li>\n<li>miTLS: <a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" href=\"http:\/\/mitls.org\" target=\"_blank\" rel=\"noopener\">mitls.org<span class=\"sr-only\"> (opens in new tab)<\/span><\/a><\/li>\n<li>KreMLin: <a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" href=\"http:\/\/github.com\/FStarLang\/kremlin\" target=\"_blank\" rel=\"noopener\">github.com\/FStarLang\/kremlin<span class=\"sr-only\"> (opens in new tab)<\/span><\/a><\/li>\n<li>HACL*: <a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" href=\"http:\/\/github.com\/project-everest\/hacl-star\" target=\"_blank\" rel=\"noopener\">github.com\/project-everest\/hacl-star<span class=\"sr-only\"> (opens in new tab)<\/span><\/a><\/li>\n<li>Vale: <a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" href=\"http:\/\/github.com\/project-everest\/vale\" target=\"_blank\" rel=\"noopener\">github.com\/project-everest\/vale<span class=\"sr-only\"> (opens in new tab)<\/span><\/a><\/li>\n<\/ul>\n<\/li>\n<li>Q#: <a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" href=\"https:\/\/github.com\/Microsoft\/qsharp-compiler\" target=\"_blank\" rel=\"noopener\">github.com\/Microsoft\/qsharp-compiler<span class=\"sr-only\"> (opens in new tab)<\/span><\/a><\/li>\n<li>TLA+: <a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" href=\"http:\/\/github.com\/tlaplus\/tlaplus\" target=\"_blank\" rel=\"noopener\">github.com\/tlaplus\/tlaplus<span class=\"sr-only\"> (opens in new tab)<\/span><\/a><\/li>\n<li>VeriSol: <a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" href=\"https:\/\/github.com\/Microsoft\/verisol\" target=\"_blank\" rel=\"noopener\">github.com\/Microsoft\/verisol<span class=\"sr-only\"> (opens in new tab)<\/span><\/a><\/li>\n<li>Z3 Theorem Prover: <a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" href=\"http:\/\/github.com\/Z3Prover\/z3\" target=\"_blank\" rel=\"noopener\">github.com\/Z3Prover\/z3<span class=\"sr-only\"> (opens in new tab)<\/span><\/a><\/li>\n<\/ul>\n<p><span id=\"label-external-link\" class=\"sr-only\" aria-hidden=\"true\">Opens in a new tab<\/span><\/p>\n<!-- \/wp:freeform --><!-- \/wp:msr\/content-tab --><!-- wp:msr\/content-tab {\"title\":\"Career opportunities\"} --><!-- wp:freeform --><p>Job openings are always searchable at <a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" href=\"https:\/\/careers.microsoft.com\/us\/en\" target=\"_blank\" rel=\"noopener\">https:\/\/careers.microsoft.com\/<span class=\"sr-only\"> (opens in new tab)<\/span><\/a> including:<\/p>\n<ul>\n<li><a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" href=\"https:\/\/careers.microsoft.com\/professionals\/us\/en\/search-results?keywords=compiler\" target=\"_blank\" rel=\"noopener\">Compiler Jobs<span class=\"sr-only\"> (opens in new tab)<\/span><\/a><\/li>\n<li><a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" href=\"https:\/\/careers.microsoft.com\/professionals\/us\/en\/search-results?keywords=runtime\" target=\"_blank\" rel=\"noopener\">Runtime Jobs<span class=\"sr-only\"> (opens in new tab)<\/span><\/a><\/li>\n<li><a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" href=\"https:\/\/careers.microsoft.com\/professionals\/us\/en\/search-results?keywords=visual%20studio\" target=\"_blank\" rel=\"noopener\">Openings in Visual Studio<span class=\"sr-only\"> (opens in new tab)<\/span><\/a><\/li>\n<li><a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" href=\"https:\/\/careers.microsoft.com\/us\/en\/job\/740235\/Principal-Software-Engineering-Manager\" target=\"_blank\" rel=\"noopener\">Visual C++ Principal Software Engineering Manager<span class=\"sr-only\"> (opens in new tab)<\/span><\/a><\/li>\n<li><a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" href=\"https:\/\/careers.microsoft.com\/us\/en\/job\/725691\/Program-Manager-2\" target=\"_blank\" rel=\"noopener\">Visual C++ Program Manager 2<span class=\"sr-only\"> (opens in new tab)<\/span><\/a><\/li>\n<\/ul>\n<p><span id=\"label-external-link\" class=\"sr-only\" aria-hidden=\"true\">Opens in a new tab<\/span><\/p>\n<!-- \/wp:freeform --><!-- \/wp:msr\/content-tab --><!-- \/wp:msr\/content-tabs -->","tab-content":[{"id":0,"name":"About","content":"The annual Symposium on Principles of Programming Languages is a forum for the discussion of all aspects of programming languages and programming systems. Both theoretical and experimental papers are welcome, on topics ranging from formal frameworks to experience reports. We seek submissions that make principled, enduring contributions to the theory, design, understanding, implementation or application of programming languages.\r\n<h3>Research Papers Program Committee Members<\/h3>\r\n<ul>\r\n \t<li><a href=\"https:\/\/www.microsoft.com\/en-us\/research\/people\/fournet\/\">C\u00e9dric Fournet<\/a><\/li>\r\n \t<li><a href=\"https:\/\/www.microsoft.com\/en-us\/research\/people\/margus\/\">Margus Veanes<\/a><\/li>\r\n \t<li><a href=\"https:\/\/www.microsoft.com\/en-us\/research\/people\/shuvendu\/\">Shuvendu K. Lahiri<\/a><\/li>\r\n<\/ul>"},{"id":1,"name":"Sessions","content":"<h2>Microsoft main conference presentation schedule<\/h2>\r\n<h3>Sunday, January 19<\/h3>\r\nProgramming Languages for Quantum Computing (PLanQC) | Workshop\r\nProgram Committee Members: <a href=\"https:\/\/www.microsoft.com\/en-us\/research\/people\/chgranad\/\">Chris Granade<\/a>, <a href=\"https:\/\/www.microsoft.com\/en-us\/research\/people\/beheim\/\">Bettina Heim<\/a>\r\n10:30 AM\u201311:00 AM, Invited talk: <a href=\"https:\/\/www.microsoft.com\/en-us\/research\/people\/beheim\/\">Bettina Heim<\/a>\r\n<h3>Monday, January 20<\/h3>\r\nPartial Evaluation and Program Manipulation (PEPM) | Workshop\r\n11:25 AM\u201312:00 PM, Panelist: <a href=\"https:\/\/www.microsoft.com\/en-us\/research\/people\/nbjorner\/\">Nikolaj Bj\u00f8rner<\/a>\r\n<h3>Tuesday, January 21<\/h3>\r\n<strong>HASE 2020 Workshop on High Assurance Systems Engineering<\/strong> | Workshop\r\nCo-organizer: <a href=\"https:\/\/www.microsoft.com\/en-us\/research\/people\/protz\/\">Jonathan Protzenko<\/a>\r\n\r\n<strong>Languages for Inference (LAFI)<\/strong> | Workshop\r\nSteering Committee Member: <a href=\"https:\/\/www.microsoft.com\/en-us\/research\/people\/adg\/\">Andrew Gordon<\/a>\r\n\r\n<strong>Programming Languages Mentoring Workshop (PLMW)<\/strong> | Workshop\r\n2:00 PM\u20133:05 PM, Panelist: <a href=\"https:\/\/www.microsoft.com\/en-us\/research\/people\/jufranc\/\">Juliana Franco<\/a>\r\n<h3>Thursday, January 23<\/h3>\r\nResearch Papers \u2013 Abstract Interpretation\r\n2:21 PM\u20132:43 PM\r\n<strong>Abstract Interpretation of Distributed Network Control Planes<\/strong>\r\n<a href=\"https:\/\/www.microsoft.com\/en-us\/research\/people\/rybecket\/\">Ryan Beckett<\/a>, Aarti Gupta, Ratul Mahajan, David Walker\r\n<h3>Saturday, January 25<\/h3>\r\n<strong>Principles of Secure Compilation (PriSC)<\/strong> | Workshop\r\nProgram Committee Member, Session Chair: <a href=\"https:\/\/www.microsoft.com\/en-us\/research\/people\/protz\/\">Jonathan Protzenko<\/a>\r\n<h2>Co-located conferences<\/h2>\r\n<h3>Monday, January 20<\/h3>\r\n<strong>22nd Symposium on Practical Aspects of Declarative Languages (PADL 2020)<\/strong>\r\n8:45 AM\u20139:35 AM, Invited Talk: <a href=\"https:\/\/www.microsoft.com\/en-us\/research\/people\/nbjorner\/\">Nikolaj Bj\u00f8rner<\/a>\r\n11:25 AM\u201312:00 PM, Panelist: <a href=\"https:\/\/www.microsoft.com\/en-us\/research\/people\/nbjorner\/\">Nikolaj Bj\u00f8rner<\/a>\r\n<h3>Tuesday, January 21<\/h3>\r\n12:00 PM\u201312:30 PM | Talk\r\n<strong>Solving LIA* Using Approximations<\/strong>\r\nMaxwell Levatich, <a href=\"https:\/\/www.microsoft.com\/en-us\/research\/people\/nbjorner\/\">Nikolaj Bj\u00f8rner<\/a>, Ruzica Piskac, Sharon Shoham"},{"id":2,"name":"Open source tools","content":"<ul>\r\n \t<li>Automata: <a href=\"http:\/\/github.com\/AutomataDotNet\/Automata\" target=\"_blank\" rel=\"noopener\">github.com\/AutomataDotNet\/Automata<\/a><\/li>\r\n \t<li>Ivy: <a href=\"http:\/\/github.com\/Microsoft\/ivy\" target=\"_blank\" rel=\"noopener\">github.com\/Microsoft\/ivy<\/a><\/li>\r\n \t<li>Lean Theorem Prover: <a href=\"http:\/\/leanprover.github.io\" target=\"_blank\" rel=\"noopener\">leanprover.github.io<\/a><\/li>\r\n \t<li>Network Verification: <a href=\"http:\/\/github.com\/Z3Prover\/\" target=\"_blank\" rel=\"noopener\">github.com\/Z3Prover\/FirewallChecker<\/a><\/li>\r\n \t<li>P\/P#: <a href=\"http:\/\/github.com\/p-org\" target=\"_blank\" rel=\"noopener\">github.com\/p-org<\/a><\/li>\r\n \t<li>Project Everest: <a href=\"http:\/\/project-everest.github.io\" target=\"_blank\" rel=\"noopener\">project-everest.github.io<\/a>\r\n<ul>\r\n \t<li>F*: <a href=\"http:\/\/fstar-lang.org\" target=\"_blank\" rel=\"noopener\">fstar-lang.org<\/a><\/li>\r\n \t<li>miTLS: <a href=\"http:\/\/mitls.org\" target=\"_blank\" rel=\"noopener\">mitls.org<\/a><\/li>\r\n \t<li>KreMLin: <a href=\"http:\/\/github.com\/FStarLang\/kremlin\" target=\"_blank\" rel=\"noopener\">github.com\/FStarLang\/kremlin<\/a><\/li>\r\n \t<li>HACL*: <a href=\"http:\/\/github.com\/project-everest\/hacl-star\" target=\"_blank\" rel=\"noopener\">github.com\/project-everest\/hacl-star<\/a><\/li>\r\n \t<li>Vale: <a href=\"http:\/\/github.com\/project-everest\/vale\" target=\"_blank\" rel=\"noopener\">github.com\/project-everest\/vale<\/a><\/li>\r\n<\/ul>\r\n<\/li>\r\n \t<li>Q#: <a href=\"https:\/\/github.com\/Microsoft\/qsharp-compiler\" target=\"_blank\" rel=\"noopener\">github.com\/Microsoft\/qsharp-compiler<\/a><\/li>\r\n \t<li>TLA+: <a href=\"http:\/\/github.com\/tlaplus\/tlaplus\" target=\"_blank\" rel=\"noopener\">github.com\/tlaplus\/tlaplus<\/a><\/li>\r\n \t<li>VeriSol: <a href=\"https:\/\/github.com\/Microsoft\/verisol\" target=\"_blank\" rel=\"noopener\">github.com\/Microsoft\/verisol<\/a><\/li>\r\n \t<li>Z3 Theorem Prover: <a href=\"http:\/\/github.com\/Z3Prover\/z3\" target=\"_blank\" rel=\"noopener\">github.com\/Z3Prover\/z3<\/a><\/li>\r\n<\/ul>"},{"id":3,"name":"Career opportunities","content":"Job openings are always searchable at <a href=\"https:\/\/careers.microsoft.com\/us\/en\" target=\"_blank\" rel=\"noopener\">https:\/\/careers.microsoft.com\/<\/a> including:\r\n<ul>\r\n \t<li><a href=\"https:\/\/careers.microsoft.com\/professionals\/us\/en\/search-results?keywords=compiler\" target=\"_blank\" rel=\"noopener\">Compiler Jobs<\/a><\/li>\r\n \t<li><a href=\"https:\/\/careers.microsoft.com\/professionals\/us\/en\/search-results?keywords=runtime\" target=\"_blank\" rel=\"noopener\">Runtime Jobs<\/a><\/li>\r\n \t<li><a href=\"https:\/\/careers.microsoft.com\/professionals\/us\/en\/search-results?keywords=visual%20studio\" target=\"_blank\" rel=\"noopener\">Openings in Visual Studio<\/a><\/li>\r\n \t<li><a href=\"https:\/\/careers.microsoft.com\/us\/en\/job\/740235\/Principal-Software-Engineering-Manager\" target=\"_blank\" rel=\"noopener\">Visual C++ Principal Software Engineering Manager<\/a><\/li>\r\n \t<li><a href=\"https:\/\/careers.microsoft.com\/us\/en\/job\/725691\/Program-Manager-2\" target=\"_blank\" rel=\"noopener\">Visual C++ Program Manager 2<\/a><\/li>\r\n<\/ul>"}],"msr_startdate":"2020-01-19","msr_enddate":"2020-01-25","msr_event_time":"","msr_location":"New Orleans, Louisiana","msr_event_link":"","msr_event_recording_link":"","msr_startdate_formatted":"January 19, 2020","msr_register_text":"Watch now","msr_cta_link":"","msr_cta_text":"","msr_cta_bi_name":"","featured_image_thumbnail":"<img width=\"960\" height=\"360\" src=\"https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2019\/03\/iclr2019_1920x720.jpg\" class=\"img-object-cover\" alt=\"New Olreans Toll Bridge over Mississippi River\" decoding=\"async\" loading=\"lazy\" srcset=\"https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2019\/03\/iclr2019_1920x720.jpg 1920w, https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2019\/03\/iclr2019_1920x720-300x113.jpg 300w, https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2019\/03\/iclr2019_1920x720-768x288.jpg 768w, https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2019\/03\/iclr2019_1920x720-1024x384.jpg 1024w, https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2019\/03\/iclr2019_1920x720-1600x600.jpg 1600w\" sizes=\"auto, (max-width: 960px) 100vw, 960px\" \/>","event_excerpt":"The annual Symposium on Principles of Programming Languages is a forum for the discussion of all aspects of programming languages and programming systems. Both theoretical and experimental papers are welcome, on topics ranging from formal frameworks to experience reports. We seek submissions that make principled, enduring contributions to the theory, design, understanding, implementation or application of programming languages.","msr_research_lab":[],"related-researchers":[],"msr_impact_theme":[],"related-academic-programs":[],"related-groups":[],"related-projects":[],"related-opportunities":[],"related-publications":[],"related-videos":[676833],"related-posts":[],"_links":{"self":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-event\/628671","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-event"}],"about":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/types\/msr-event"}],"version-history":[{"count":4,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-event\/628671\/revisions"}],"predecessor-version":[{"id":1147003,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-event\/628671\/revisions\/1147003"}],"wp:featuredmedia":[{"embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/media\/571890"}],"wp:attachment":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/media?parent=628671"}],"wp:term":[{"taxonomy":"msr-research-area","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/research-area?post=628671"},{"taxonomy":"msr-region","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-region?post=628671"},{"taxonomy":"msr-event-type","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-event-type?post=628671"},{"taxonomy":"msr-video-type","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-video-type?post=628671"},{"taxonomy":"msr-locale","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-locale?post=628671"},{"taxonomy":"msr-program-audience","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-program-audience?post=628671"},{"taxonomy":"msr-post-option","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-post-option?post=628671"},{"taxonomy":"msr-impact-theme","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-impact-theme?post=628671"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}