BibSLEIGH — Lars

Travelled to:

1 × Cyprus
1 × Estonia
1 × Hungary
1 × Iceland
1 × India
1 × Japan
1 × Norway
1 × Serbia
1 × Slovenia
12 × USA
2 × Austria
2 × Canada
2 × Germany
2 × Spain
3 × France
3 × Italy
3 × Portugal
4 × United Kingdom

Collaborated with:

K.Svendsen J.Schwinghammer H.Yang A.Bizjak D.Dreyer J.Thamsborg A.Nanevski M.J.Parkinson K.Støvring F.Sieczkowski G.Morrisett ∅ N.Torp-Smith M.Welinder B.Reus A.Ahmed R.E.Møgelberg R.Krebbers L.Skorstengaard D.Devriese G.Neis Amin Timany Morten Krogh-Jespersen J.B.Jensen A.Bauer A.Turon T.Dinsdale-Young R.Clouston H.B.Grathwohl M.Miculan B.Biering J.C.Reynolds M.Tofte M.Vejlstrup J.Pichon-Pharabod A.Rossberg R.L.Petersen A.Carboni G.Rosolini D.S.Scott P.d.R.Pinto K.J.Andersen L.Stefanesco Daniel Gratzer P.Gardner A.J.Turon F.Pottier A.Shinnar P.Govereau S.Debois E.Elsborg T.T.Hildebrandt H.Niss R.J.0002 J.Jourdan A.A.0001 G.Barthe M.Gaboardi D.G.0001 B.Spitters A.Vezzosi R.Jung D.Swasey

Talks about:

logic (20) type (15) concurr (14) higher (13) order (13) separ (12) relat (12) reason (11) step (9) theori (8)

Person: Lars Birkedal

DBLP: Birkedal:Lars

Facilitated 1 volumes:

Contributed to:

2015

2014

2013

2012

2011

2010

2009

2008

2007

2006

2005

2004

2000

1998

1996

1994

2016

2017

2018

2016

2017

2018

2019

Wrote 55 papers:

ESOP-2015-SieczkowskiSBP #consistency #logic: A Separation Logic for Fictional Sequential Consistency (FS, KS, LB, JPP), pp. 736–761.
FoSSaCS-2015-BizjakB #logic #probability: Step-Indexed Logical Relations for Probability (AB, LB), pp. 279–294.
FoSSaCS-2015-CloustonBGB #induction #programming #reasoning #recursion: Programming and Reasoning with Guarded Recursion for Coinductive Types (RC, AB, HBG, LB), pp. 407–421.
POPL-2015-JungSSSTBD #concurrent #invariant #monad #named #orthogonal #reasoning: Iris: Monoids and Invariants as an Orthogonal Basis for Concurrent Reasoning (RJ, DS, FS, KS, AT, LB, DD), pp. 637–650.
ESOP-2014-SvendsenB #concurrent: Impredicative Concurrent Abstract Predicates (KS, LB), pp. 149–168.
POPL-2014-Birkedal #composition #concurrent #higher-order #imperative #reasoning #source code: Modular reasoning about concurrent higher-order imperative programs (LB), pp. 1–2.
RTA-TLCA-2014-BizjakBM #nondeterminism #type system: A Model of Countable Nondeterminism in Guarded Type Theory (AB, LB, MM), pp. 108–123.
ECOOP-2013-SvendsenBP #case study #composition #concurrent #higher-order #library #named #specification: Joins: A Case Study in Modular Specification of a Concurrent Reentrant Higher-Order Library (KS, LB, MJP), pp. 327–351.
ESOP-2013-SvendsenBP #composition #concurrent #data type #reasoning: Modular Reasoning about Separation of Concurrent Data Structures (KS, LB, MJP), pp. 169–188.
ICFP-2013-TuronDB #concurrent #higher-order #hoare #logic #reasoning #refinement: Unifying refinement and hoare-style reasoning in a logic for higher-order concurrency (AT, DD, LB), pp. 377–390.
LICS-2013-BirkedalM #fixpoint #recursion #type system: Intensional Type Theory with Guarded Recursive Types qua Fixed Points on Universes (LB, REM), pp. 213–222.
POPL-2013-Dinsdale-YoungBGPY #composition #concurrent #named #reasoning #source code: Views: compositional reasoning for concurrent programs (TDY, LB, PG, MJP, HY), pp. 287–300.
POPL-2013-TuronTABD #concurrent #fine-grained #logic: Logical relations for fine-grained concurrency (AJT, JT, AA, LB, DD), pp. 343–356.
CSL-2012-BirkedalST #concurrent #logic: A Concurrent Logical Relation (LB, FS, JT), pp. 107–121.
ESOP-2012-JensenB #logic: Fictional Separation Logic (JBJ, LB), pp. 377–396.
CSL-2011-SchwinghammerB #nondeterminism #reasoning #relational: Step-Indexed Relational Reasoning for Countable Nondeterminism (JS, LB), pp. 512–524.
FoSSaCS-2011-SchwinghammerBS #metric #recursion: A Step-Indexed Kripke Model of Hidden State via Recursive Properties on Recursively Defined Metric Spaces (JS, LB, KS), pp. 305–319.
ICFP-2011-ThamsborgB #logic #program transformation: A kripke logical relation for effect-based program transformations (JT, LB), pp. 445–456.
LICS-2011-BirkedalMSS: First Steps in Synthetic Guarded Domain Theory: Step-Indexing in the Topos of Trees (LB, REM, JS, KS), pp. 55–64.
POPL-2011-BirkedalRSSTY #modelling #recursion: Step-indexed kripke models over recursive worlds (LB, BR, JS, KS, JT, HY), pp. 119–132.
TLCA-2011-SvendsenBN #dependent type: Partiality, State and Dependent Types (KS, LB, AN), pp. 198–212.
ECOOP-2010-SvendsenBP #verification: Verifying Generics and Delegates (KS, LB, MJP), pp. 175–199.
FoSSaCS-2010-SchwinghammerYBPR #semantics: A Semantic Foundation for Hidden State (JS, HY, LB, FP, BR), pp. 2–17.
ICFP-2010-DreyerNB #higher-order #reasoning #relational: The impact of higher-order state and control effects on local relational reasoning (DD, GN, LB), pp. 143–156.
POPL-2010-DreyerNRB #data type #higher-order #logic #relational: A relational modal logic for higher-order stateful ADTs (DD, GN, AR, LB), pp. 185–198.
CSL-2009-SchwinghammerBRY #higher-order #hoare: Nested Hoare Triples and Frame Rules for Higher-Order Store (JS, LB, BR, HY), pp. 440–454.
FoSSaCS-2009-BirkedalST #morphism #parametricity #polymorphism #recursion #semantics: Realizability Semantics of Parametric Polymorphism, General References, and Recursive Types (LB, KS, JT), pp. 456–470.
LICS-2009-DreyerAB #logic: Logical Step-Indexed Logical Relations (DD, AA, LB), pp. 71–80.
ESOP-2008-PetersenBNM #hoare #type system: A Realizability Model for Impredicative Hoare Type Theory (RLP, LB, AN, GM), pp. 337–352.
ICALP-B-2008-BirkedalRSY #higher-order #logic: A Simple Model of Separation Logic for Higher-Order Store (LB, BR, JS, HY), pp. 348–360.
ICFP-2008-NanevskiMSGB #dependent type #imperative #named #source code: Ynot: dependent types for imperative programs (AN, GM, AS, PG, LB), pp. 229–240.
ESOP-2007-NanevskiAMB #data type #hoare #type system: Abstract Predicates and Mutable ADTs in Hoare Type Theory (AN, AA, GM, LB), pp. 189–204.
FoSSaCS-2007-BirkedalY #logic #parametricity #relational: Relational Parametricity and Separation Logic (LB, HY), pp. 93–107.
FoSSaCS-2006-BirkedalDEHN #modelling: Bigraphical Models of Context-Aware Systems (LB, SD, EE, TTH, HN), pp. 187–201.
ICFP-2006-NanevskiMB #hoare #morphism #polymorphism #type system: Polymorphism and separation in hoare type theory (AN, GM, LB), pp. 62–73.
ESOP-2005-BieringBT #higher-order #logic: BI Hyperdoctrines and Higher-Order Separation Logic (BB, LB, NTS), pp. 233–247.
LICS-2005-BirkedalTY #higher-order #semantics #type system: Semantics of Separation-Logic Typing and Higher-Order Frame Rules (LB, NTS, HY), pp. 260–269.
POPL-2004-BirkedalTR #garbage collection #reasoning: Local reasoning about a copying garbage collector (LB, NTS, JCR), pp. 220–231.
CSL-2000-BauerB #dependent type: Continuous Functionals of Dependent Types and Equilogical Spaces (AB, LB), pp. 202–216.
LICS-2000-Birkedal: A General Notion of Realizability (LB), pp. 7–17.
LICS-1998-BirkedalCRS #category theory #type system: Type Theory via Exact Categories (LB, AC, GR, DSS), pp. 188–198.
POPL-1996-BirkedalTV #representation: From Region Inference to von Neumann Machines via Region Representation Inference (LB, MT, MV), pp. 171–183.
PEPM-1994-BirkedalW #analysis #ml #standard: Binding-Time Analysis for Standard ML (LB, MW), pp. 61–71.
PLILP-1994-BirkedalW #generative: Hand-Writing Program Generator Generators (LB, MW), pp. 198–214.
ESOP-2016-SvendsenSB #logic: Transfinite Step-Indexing: Decoupling Concrete and Logical Steps (KS, FS, LB), pp. 727–751.
ESOP-2017-Dinsdale-YoungP #automation #concurrent #fine-grained #verification: Caper - Automatic Verification for Fine-Grained Concurrency (TDY, PdRP, KJA, LB), pp. 420–447.
ESOP-2017-Krebbers0BJDB #concurrent #higher-order #logic: The Essence of Higher-Order Concurrent Separation Logic (RK, RJ0, AB, JHJ, DD, LB), pp. 696–723.
ESOP-2018-0001BBBG0 #markov #probability #reasoning #relational #λ-calculus: Relational Reasoning for Markov Chains in a Probabilistic Guarded Lambda Calculus (AA0, GB, LB, AB, MG, DG0), pp. 214–241.
ESOP-2018-SkorstengaardDB #pointer #reasoning #stack: Reasoning About a Machine with Local Capabilities - Provably Safe Stack and Return Pointer Management (LS, DD, LB), pp. 475–501.
CSL-2016-BirkedalBCGSV #recursion #similarity #type system: Guarded Cubical Type Theory: Path Equality for Guarded Recursion (LB, AB, RC, HBG, BS, AV), p. 17.
POPL-2017-KrebbersTB #concurrent #higher-order #interactive #logic #proving: Interactive proofs in higher-order concurrent separation logic (RK, AT, LB), pp. 205–217.
POPL-2017-Krogh-Jespersen #concurrent #higher-order #logic #relational: A relational model of types-and-effects in higher-order concurrent separation logic (MKJ, KS, LB), pp. 218–231.
POPL-2018-TimanySKB #encapsulation #logic #monad #proving: A logical relation for monadic encapsulation of state: proving contextual equivalences in the presence of runST (AT, LS, MKJ, LB), p. 28.
POPL-2019-BizjakGKB #concurrent #higher-order #logic #named: Iron: managing obligations in higher-order concurrent separation logic (AB, DG, RK, LB), p. 30.
POPL-2019-SkorstengaardDB #control flow #encapsulation #linear #named #stack #using: StkTokens: enforcing well-bracketed control flow and stack encapsulation using linear capabilities (LS, DD, LB), p. 28.