Favorites

I keep a list of papers that I find and found interesting. If you enjoy reading as much as I do, you might want to check them out, too. Below you will find a short summary of the methods and possible applications, followed by the list of papers.

methods

interpreters

compilers

intermediate representations

effects

confidence (proof > probability > test)

possible applications

recommended papers (sorted by year of publication)

Do Judge a Test by its Cover. 2021. ESOP. Goldstein, Hughes , Lampropoulos, Pierce https://dx.doi.org/10.1007/978-3-030-72019-3_10

For a Few Dollars More. 2021. ESOP. Haslbeck, Lammich https://dx.doi.org/10.1007/978-3-030-72019-3_11

A Study of Continuous Vector Representationsfor Theorem Proving. 2021. ArXiv. Purgal, Parsert, Kaliszyk https://dx.doi.org/10.1093/logcom/exab006

Diamonds are not forever: liveness in reactive programming with guarded recursion. 2021. Proc ACM Program Lang. Bahr, Graulund, Møgelberg https://dx.doi.org/10.1145/3434283

𝜆ₛ: computable semantics for differentiable programming with higher-order functions and datatypes. 2021. Proc ACM Program Lang. Sherman, Michel, Carbin https://dx.doi.org/10.1145/3434284

Transfinite step-indexing for termination. 2021. Proc ACM Program Lang. Spies, Krishnaswami, Dreyer https://dx.doi.org/10.1145/3434294

Intrinsically typed compilation with nameless labels. 2021. . Rouvoet, Krebbers , Visser https://dx.doi.org/10.1145/3434303

egg: Fast and extensible equality saturation. 2021. Proc ACM Program Lang. Willsey, Nandi, Wang, Flatt, Tatlock , Panchekha https://dx.doi.org/10.1145/3434304

Paradoxes of probabilistic programming: and how to condition on events of measure zero with infinitesimal probabilities. 2021. Proc ACM Program Lang. Jacobs https://dx.doi.org/10.1145/3434339

The taming of the rew: a type theory with computational assumptions. 2021. Proc ACM Program Lang. Cockx , Tabareau, Winterhalter https://dx.doi.org/10.1145/3434341

An Incentive-Compatible Smart Contract for Decentralized Commerce. 2021. IACR Cryptol ePrint Arch. Schwartzbach https://arxiv.org/abs/2008.10326

Termination Analysis Without the Tears. 2021. ArXiv. Zhu, Kincaid https://arxiv.org/abs/2101.09783

Functional Extensionality for Refinement Types. 2021. ArXiv. Vazou , Greenberg https://arxiv.org/abs/2103.02177

Zooid: a DSL for Certified Multiparty Computation. 2021. ArXiv. Castro-Perez, Ferreira, Gheri, Yoshida https://arxiv.org/abs/2103.10269

Security Properties as Nested Causal Statements. 2021. ArXiv. Soloviev, Halpern https://arxiv.org/abs/2104.00872

Proving the Safety of Highly-Available Distributed Objects. 2020. ESOP. Nair, Petri, Shapiro https://dx.doi.org/10.1007/978-3-030-44914-8_20

Mixed Sessions. 2020. ESOP. Vasconcelos, Casal, Almeida, Mordido https://dx.doi.org/10.1007/978-3-030-44914-8_26

On the Versatility of Open Logical Relations. 2020. ESOP. Barthe, Crubill’e, Lago, Gavazzo https://dx.doi.org/10.1007/978-3-030-44914-8_3

Liberate Abstract Garbage Collection from the Stack by Decomposing the Heap. 2020. ESOP. Germane, Adams https://dx.doi.org/10.1007/978-3-030-44914-8_8

SoK: Layer-Two Blockchain Protocols. 2020. Financial Cryptography. Gudgeon, Moreno-Sanchez, Roos, McCorry, Gervais https://dx.doi.org/10.1007/978-3-030-51280-4_12

Fractional Types. 2020. RC. Chen, Choudhury, Carette, Sabry https://dx.doi.org/10.1007/978-3-030-52482-1_10

A categorical approach to secure compilation. 2020. CMCS. Tsampas, Nuyts, Devriese, Piessens https://dx.doi.org/10.1007/978-3-030-57201-3_9

One-Shot Algebraic Effects as Coroutines. 2020. TFP. Kawahara, Kameyama https://dx.doi.org/10.1007/978-3-030-57761-2_8

Session Types Without Sophistry - System Description. 2020. FLOPS. Kiselyov, Imai https://dx.doi.org/10.1007/978-3-030-59025-3_5

A Set-Based Context Model for Program Analysis. 2020. APLAS. Facchinetti, Palmer, Smith, Wu, Yorihiro https://dx.doi.org/10.1007/978-3-030-64437-6_1

Lightweight Virtual Payment Channels. 2020. IACR Cryptol ePrint Arch. Jourenko, Larangeira, Tanaka https://dx.doi.org/10.1007/978-3-030-65411-5_18

Cost Analysis of Smart Contracts Via Parametric Resource Analysis. 2020. SAS. Pérez, Klemen, Lopez-García, Morales, Hermenegildo https://dx.doi.org/10.1007/978-3-030-65474-0_2

The MetaCoq Project. 2020. Journal of Automated Reasoning. Sozeau, Anand, Boulier, Cohen, Forster, Kunze, Malecha, Tabareau, Winterhalter https://dx.doi.org/10.1007/s10817-019-09540-0

Programming language foundations in Agda. 2020. Sci Comput Program. Kokke, Siek , Wadler https://dx.doi.org/10.1016/J.SCICO.2020.102440

Agda Formalization of a Security-preserving Translation from Flow-sensitive to Flow-insensitive Security Types. 2020. . Manzino, Pardo https://dx.doi.org/10.1016/j.entcs.2020.08.005

Prime clock: Encoded vector clock to characterize causality in distributed systems. 2020. J Parallel Distributed Comput. Kshemkalyani , Shen, Voleti https://dx.doi.org/10.1016/j.jpdc.2020.02.008

Probabilistic data structures for big data analytics: A comprehensive review. 2020. Knowl Based Syst. Singh, Garg, Kaur, Batra, Kumar, Zomaya https://dx.doi.org/10.1016/j.knosys.2019.104987

Pallene: A companion language for Lua. 2020. Sci Comput Program. Gualandi, Ierusalimschy https://dx.doi.org/10.1016/j.scico.2020.102393

The optics of language-integrated query. 2020. Sci Comput Program. López-González, Serrano https://dx.doi.org/10.1016/j.scico.2020.102395

Transparent replication using metaprogramming in Cyan. 2020. . Ugliara, Vieira, Guimarães https://dx.doi.org/10.1016/j.scico.2020.102531

Elaborating dependent (co)pattern matching: No pattern left behind. 2020. Journal of Functional Programming. Cockx , Abel https://dx.doi.org/10.1017/S0956796819000182

Effekt: Capability-passing style for type- and effect-safe, extensible effect handlers in Scala. 2020. Journal of Functional Programming. Brachthäuser, Schuster, Ostermann https://dx.doi.org/10.1017/S0956796820000027

Effekt: Capability-passing style for type- and effect-safe, extensible effect handlers in Scala. 2020. J Funct Program. Brachthäuser, Schuster, Ostermann https://dx.doi.org/10.1017/s0956796820000027

Online Payments by Merely Broadcasting Messages. 2020. DSN. Collins, Guerraoui, Komatovic, Kuznetsov, Monti, Pavlovic, Pignolet, Seredinschi, Tonkikh, Xygkis https://dx.doi.org/10.1109/DSN48063.2020.00023

Demystifying Loops in Smart Contracts. 2020. ASE. Mariano, Chen, Feng, Lahiri, Dillig https://dx.doi.org/10.1145/3324884.3416626

A wait-free universal construction for large objects. 2020. PPoPP. Correia, Ramalhete, Felber https://dx.doi.org/10.1145/3332466.3374523

Persistent memory and the rise of universal constructions. 2020. EuroSys. Correia, Felber, Ramalhete https://dx.doi.org/10.1145/3342195.3387515

A Survey of Metaprogramming Languages. 2020. ACM Comput Surv. Lilis, Savidis https://dx.doi.org/10.1145/3354584

Actris: session-type based reasoning in separation logic. 2020. Proc ACM Program Lang. Hinrichsen, Bengtson, Krebbers https://dx.doi.org/10.1145/3371074

Incorrectness logic. 2020. Proc ACM Program Lang. O’Hearn https://dx.doi.org/10.1145/3371078

Decomposition diversity with symmetric data and codata. 2020. Proc ACM Program Lang. Binder, Jabs, Skupin, Ostermann https://dx.doi.org/10.1145/3371098

A simple differentiable programming language. 2020. Proc ACM Program Lang. Abadi, Plotkin https://dx.doi.org/10.1145/3371106

Interaction trees: representing recursive and impure programs in Coq. 2020. Proc ACM Program Lang. Xia, Zakowski, He, Hur, Malecha, Pierce, Zdancewic https://dx.doi.org/10.1145/3371119

A probabilistic separation logic. 2020. Proc ACM Program Lang. Barthe, Hsu, Liao https://dx.doi.org/10.1145/3371123

FreeSpec: specifying, verifying, and executing impure computations in Coq. 2020. CPP. Letan, Régis-Gianas https://dx.doi.org/10.1145/3372885.3373812

Coq à la carte: a practical approach to modular syntax with binders. 2020. CPP. Forster, Stark https://dx.doi.org/10.1145/3372885.3373817

Intrinsically-typed definitional interpreters for linear, session-typed languages. 2020. CPP. Rouvoet, Poulsen, Krebbers, Visser https://dx.doi.org/10.1145/3372885.3373818

HEAX: An Architecture for Computing on Encrypted Data. 2020. ASPLOS. Riazi, Laine, Pelton, Dai https://dx.doi.org/10.1145/3373376.3378523

Compiling first-order functions to session-typed parallel code. 2020. CC. Castro-Perez, Yoshida https://dx.doi.org/10.1145/3377555.3377889

Aspect-oriented language for reactive distributed applications at the edge. 2020. EdgeSys@EuroSys. Kuraj, Solar-Lezama https://dx.doi.org/10.1145/3378679.3394531

Chronofold: a data structure for versioned text. 2020. PaPoC@EuroSys. Grishchenko, Patrakeev https://dx.doi.org/10.1145/3380787.3393680

Paxos vs Raft: have we reached consensus on distributed consensus?. 2020. PaPoC@EuroSys. Howard, Mortier https://dx.doi.org/10.1145/3380787.3393681

Composing and decomposing op-based CRDTs with semidirect products: (summary). 2020. PaPoC@EuroSys. Weidner, Miller , Meiklejohn https://dx.doi.org/10.1145/3380787.3393687

Garbage collection using a finite liveness domain. 2020. ISMM. Bansal, Goel, Shah, Sanyal, Kumar https://dx.doi.org/10.1145/3381898.3397208

Securing smart contract with runtime validation. 2020. PLDI. Li, Choi, Long https://dx.doi.org/10.1145/3385412.3385982

EVA: an encrypted vector arithmetic language and compiler for efficient homomorphic computation. 2020. PLDI. Dathathri, Kostova, Saarikivi, Dai, Laine, Musuvathi https://dx.doi.org/10.1145/3385412.3386023

A Survey of Multitier Programming. 2020. ACM Comput Surv. Weisenburger, Wirth, Salvaneschi https://dx.doi.org/10.1145/3397495

A graded monad for deadlock-free concurrency (functional pearl). 2020. Haskell@ICFP. Ivaskovic, Mycroft https://dx.doi.org/10.1145/3406088.3409024

A dependently typed calculus with pattern matching and erasure inference. 2020. Proc ACM Program Lang. Tejiščák https://dx.doi.org/10.1145/3408973

Achieving high-performance the functional way: a functional pearl on expressing high-performance optimizations as rewrite strategies. 2020. Proc ACM Program Lang. Hagedorn, Lenfers, Köhler, Qin, Gorlatch, Steuwer https://dx.doi.org/10.1145/3408974

Cosmo: a concurrent separation logic for multicore OCaml. 2020. Proc ACM Program Lang. Mével, Jourdan, Pottier https://dx.doi.org/10.1145/3408978

Effect handlers, evidently. 2020. Proc ACM Program Lang. Xie, Brachthäuser, Hillerström, Schuster, Leijen https://dx.doi.org/10.1145/3408981

Kinds are calling conventions. 2020. Proc ACM Program Lang. Downen, Ariola, Jones, Eisenberg https://dx.doi.org/10.1145/3408986

Separation logic for sequential programs (functional pearl). 2020. Proc ACM Program Lang. Charguéraud https://dx.doi.org/10.1145/3408998

SteelCore: an extensible concurrent separation logic for effectful dependently typed programs. 2020. Proc ACM Program Lang. Swamy, Rastogi, Fromherz, Merigoux, Ahman, Martínez https://dx.doi.org/10.1145/3409003

A Computational Understanding of Classical (Co)Recursion. 2020. PPDP. Downen, Ariola https://dx.doi.org/10.1145/3414080.3414086

Multi-stage programming in the large with staged classes. 2020. . Parreaux, Shaikhha https://dx.doi.org/10.1145/3425898.3426961

Extrinsically typed operational semantics for functional languages. 2020. SLE. Cimini, Miller, Siek https://dx.doi.org/10.1145/3426425.3426936

Effects as capabilities: effect handlers and lightweight effect polymorphism. 2020. . Immanuel, SchusterPhilipp, OstermannKlaus https://dx.doi.org/10.1145/3428194

Compiling symbolic execution with staging and algebraic effects. 2020. Proc ACM Program Lang. Wei, Bracevac, Tan, Rompf https://dx.doi.org/10.1145/3428232

Programming at the edge of synchrony. 2020. Proc ACM Program Lang. Dragoi, Widder, Zufferey https://dx.doi.org/10.1145/3428281

Data-Flow Analyses as Effects and Graded Monads. 2020. FSCD. Ivaskovic, Mycroft, Orchard https://dx.doi.org/10.4230/LIPIcs.FSCD.2020.15

A Reflection on Continuation-Composing Style. 2020. FSCD. Biernacki , Pyzik, Sieczkowski https://dx.doi.org/10.4230/LIPIcs.FSCD.2020.18

Heterogeneous Paxos. 2020. OPODIS. Sheff, Wang, Renesse, Myers https://dx.doi.org/10.4230/LIPIcs.OPODIS.2020.5

Contra: A Programmable System for Performance-aware Routing. 2020. NSDI. Hsu, Beckett, Chen, Rexford, Tammana, Walker https://arxiv.org/abs/1902.00849

Proving properties of polymorphic programs using type isomorphisms with the Yoneda lemma.. 2020. . Pistone, Tranchini https://arxiv.org/abs/1907.03481

Notes on Theory of Distributed Systems. 2020. ArXiv. Aspnes https://arxiv.org/abs/2001.04235

Blockchain Consensus Algorithms: A Survey. 2020. . Ferdous, Chowdhury, Hoque, Colman https://arxiv.org/abs/2001.07091

Profunctor optics, a categorical update. 2020. ArXiv. Clarke, Elkins, Gibbons , Loregiàn, Milewski, Pillmore, Román https://arxiv.org/abs/2001.07488

Why Should Anyone use Colours? or, Syntax Highlighting Beyond Code Snippets. 2020. ArXiv. Patrignani https://arxiv.org/abs/2001.11334

Proving the Lottery Ticket Hypothesis: Pruning is All You Need. 2020. ArXiv. Malach, Yehudai, Shalev-Shwartz , Shamir https://arxiv.org/abs/2002.00585

Patterns for Name Analysis and Type Analysis with JastAdd. 2020. ArXiv. Meyer, Pfarr https://arxiv.org/abs/2002.01842

The Bloom Tree. 2020. ArXiv. Ramabaja, Avdullahu https://arxiv.org/abs/2002.03057

Path homology as a stronger analogue of cyclomatic complexity. 2020. . Huntsman https://arxiv.org/abs/2003.00944

A Formalization of SQL with Nulls. 2020. ArXiv. Ricciotti, Cheney https://arxiv.org/abs/2003.11331

UTxO- vs account-based smart contract blockchain programming paradigms. 2020. ArXiv. Brünjes, Gabbay https://arxiv.org/abs/2003.14271

Merkle-CRDTs: Merkle-DAGs meet CRDTs. 2020. ArXiv. Sanjuán, Poyhtari, Teixeira, Psaras https://arxiv.org/abs/2004.00107

egg: Easy, Efficient, and Extensible E-graphs. 2020. ArXiv. Willsey, Wang, Flatt, Nandi, Panchekha , Tatlock https://arxiv.org/abs/2004.03082

Consensus for Crosschain Communications. 2020. ArXiv. Robinson https://arxiv.org/abs/2004.09494

Dynamic IFC Theorems for Free!. 2020. ArXiv. Algehed, Bernardy, Hritcu https://arxiv.org/abs/2005.04722

{\pi} with leftovers: a mechanisation in Agda. 2020. . Zalakain, Dardha https://arxiv.org/abs/2005.05902

How to generate random lambda terms?. 2020. ArXiv. Bendkowski https://arxiv.org/abs/2005.08856

Choreographies as Objects. 2020. ArXiv. Giallorenzo, Montesi, Peressotti https://arxiv.org/abs/2005.09520

Reinforcement Learning Under Moral Uncertainty. 2020. ArXiv. Ecoffet, Lehman https://arxiv.org/abs/2006.04734

Formalizing Nakamoto-Style Proof of Stake. 2020. IACR Cryptol ePrint Arch. Thomsen, Spitters https://arxiv.org/abs/2007.12105

Logical Relations as Types: Proof-Relevant Parametricity for Program Modules. 2020. ArXiv. Sterling, Harper https://arxiv.org/abs/2010.08599

Neural Teleportation. 2020. ArXiv. Armenta, Judge, Painchaud, Skandarani, Lemaire, Sanchez, Spino, Jodoin https://arxiv.org/abs/2012.01118

Codata in Action. 2019. ESOP. Downen, Sullivan, Ariola , Jones https://dx.doi.org/10.1007/978-3-030-17184-1_5

Featherweight Scribble. 2019. Models Languages and Tools for Concurrent and Distributed Programming. Neykova, Yoshida https://dx.doi.org/10.1007/978-3-030-21485-2_14

Automated Hypersafety Verification. 2019. CAV. Farzan , Vandikas https://dx.doi.org/10.1007/978-3-030-25540-4_11

A Formalized General Theory of Syntax with Bindings: Extended Version. 2019. Journal of Automated Reasoning. Gheri, Popescu https://dx.doi.org/10.1007/s10817-019-09522-2

The verified CakeML compiler backend. 2019. J Funct Program. Tan, Myreen, Kumar, Fox, Owens , Norrish https://dx.doi.org/10.1017/S0956796818000229

A theory of RPC calculi for client-server model. 2019. J Funct Program. Choi, Chang https://dx.doi.org/10.1017/S0956796819000029

A SQL to C compiler in 500 lines of code. 2019. J Funct Program. Rompf , Amin https://dx.doi.org/10.1017/S0956796819000054

Journey Beyond Full Abstraction: Exploring Robust Property Preservation for Secure Compilation. 2019. CSF. Abate, Blanco, Garg, Hritcu, Patrignani, Thibault https://dx.doi.org/10.1109/CSF.2019.00025

Using Information Flow to Design an ISA that Controls Timing Channels. 2019. CSF. Zagieboylo, Suh, Myers https://dx.doi.org/10.1109/CSF.2019.00026

Separation logic. 2019. Commun ACM. O’Hearn https://dx.doi.org/10.1145/3211968

Context-Free Session Type Inference. 2019. TOPL. Padovani https://dx.doi.org/10.1145/3229062

Definitional proof-irrelevance without K. 2019. Proc ACM Program Lang. Gilbert, Cockx , Sozeau, Tabareau https://dx.doi.org/10.1145/3290316

code2vec: learning distributed representations of code. 2019. Proc ACM Program Lang. Alon, Zilberstein, Levy, Yahav https://dx.doi.org/10.1145/3290353

Closed forms for numerical loops. 2019. Proc ACM Program Lang. Kincaid , Breck, Cyphert, Reps https://dx.doi.org/10.1145/3290368

Pretend synchrony: synchronous verification of asynchronous distributed programs. 2019. Proc ACM Program Lang. Gleissenthall, Kici, Bakst, Stefan, Jhala https://dx.doi.org/10.1145/3290372

Composable, sound transformations of nested recursion and loops. 2019. PLDI. Sundararajah, Kulkarni https://dx.doi.org/10.1145/3314221.3314592

ILC: a calculus for composable, computational cryptography. 2019. IACR Cryptol ePrint Arch. Liao, Hammer, Miller https://dx.doi.org/10.1145/3314221.3314607

Verifying message-passing programs with dependent behavioural types. 2019. PLDI. Scalas, Yoshida , Benussi https://dx.doi.org/10.1145/3314221.3322484

The next 700 compiler correctness theorems (functional pearl). 2019. Proc ACM Program Lang. Patterson, Ahmed https://dx.doi.org/10.1145/3341689

Simple noninterference from parametricity. 2019. Proc ACM Program Lang. Algehed, Bernardy https://dx.doi.org/10.1145/3341693

Demystifying differentiable programming: shift/reset the penultimate backpropagator. 2019. Proc ACM Program Lang. Wang, Wu, Essertel, Decker, Rompf https://dx.doi.org/10.1145/3341700

A predicate transformer semantics for effects (functional pearl). 2019. Proc ACM Program Lang. Swierstra, Baanen https://dx.doi.org/10.1145/3341707

Property-Based Testing via Proof Reconstruction. 2019. PPDP. Blanco, Miller, Momigliano https://dx.doi.org/10.1145/3354166.3354170

Intrinsically-Typed Mechanized Semantics for Session Types. 2019. PPDP. Thiemann https://dx.doi.org/10.1145/3354166.3354184

Exponential Elimination for Bicartesian Closed Categorical Combinators. 2019. PPDP. Valliappan, Russo https://dx.doi.org/10.1145/3354166.3354185

From definitional interpreter to symbolic executor. 2019. META. Mensing, Antwerpen, Poulsen , Visser https://dx.doi.org/10.1145/3358502.3361269

Reliable and fast DWARF-based stack unwinding. 2019. Proc ACM Program Lang. Bastian, Kell , Nardelli https://dx.doi.org/10.1145/3360572

Xor Filters: Faster and Smaller Than Bloom and Cuckoo Filters. 2019. ArXiv. Graf, Lemire https://dx.doi.org/10.1145/3376122

Composition of Languages Embedded in Scala. 2019. FedCSIS. Haeri, Keir https://dx.doi.org/10.15439/2019F61

Bisimulations for Delimited-Control Operators. 2019. Log Methods Comput Sci. Biernacki , Lenglet, Polesiuk https://dx.doi.org/10.23638/LMCS-15(2:18)2019

Value-Dependent Session Design in a Dependently Typed Language. 2019. PLACES@ETAPS. Muijnck-Hughes, Brady, Vanderbauwhede https://dx.doi.org/10.4204/EPTCS.291.5

A Program Logic for First-Order Encapsulated WebAssembly. 2019. ECOOP. Watt, Maksimovic, Krishnaswami, Gardner https://dx.doi.org/10.4230/LIPIcs.ECOOP.2019.9

An Efficient Universal Construction for Large Objects. 2019. OPODIS. Fatourou, Kallimanis, Kanellou https://dx.doi.org/10.4230/LIPIcs.OPODIS.2019.18

Type Theory Unchained: Extending Agda with User-Defined Rewrite Rules. 2019. TYPES. Cockx https://dx.doi.org/10.4230/LIPIcs.TYPES.2019.2

Eliom: A Language for Modular Tierless Web Programming. 2019. ArXiv. Radanne, Vouillon, Balat https://arxiv.org/abs/1901.11411

Practical Sized Typing for Coq. 2019. ArXiv. Chan, Bowman https://arxiv.org/abs/1912.05601

HOBiT: Programming Lenses Without Using Lens Combinators. 2018. ESOP. Matsuda, Wang https://dx.doi.org/10.1007/978-3-319-89884-1_2

Backwards and Forwards with Separation Logic. 2018. ITP. Bannister, Höfner, Klein https://dx.doi.org/10.1007/978-3-319-94821-8_5

Random generation of closed simply typed λ-terms: A synergy between logic programming and Boltzmann samplers. 2018. Theory Pract Log Program. Bendkowski, Grygiel, Tarau https://dx.doi.org/10.1017/S147106841700045X

ZoKrates - Scalable Privacy-Preserving Off-Chain Computations. 2018. SmartData. Eberhardt, Tai https://dx.doi.org/10.1109/Cybermatics_2018.2018.00199

Unifying analytic and statically-typed quasiquotes. 2018. Proc ACM Program Lang. Parreaux, Voizard, Shaikhha, Koch https://dx.doi.org/10.1145/3158101

Generating good generators for inductive relations. 2018. Proc ACM Program Lang. Lampropoulos, Paraskevopoulou, Pierce https://dx.doi.org/10.1145/3158133

Collapsing towers of interpreters. 2018. Proc ACM Program Lang. Amin , Rompf https://dx.doi.org/10.1145/3158140

Selective CPS transformation for shift and reset. 2018. PEPM. Asai, Uehara https://dx.doi.org/10.1145/3162069

Incremental relational lenses. 2018. Proc ACM Program Lang. Horn, Perera, Cheney https://dx.doi.org/10.1145/3236769

A type and scope safe universe of syntaxes with binding: their semantics and proofs. 2018. Proc ACM Program Lang. Allais, Atkey, Chapman, McBride, McKinna https://dx.doi.org/10.1145/3236785

Refunctionalization of abstract abstract machines: bridging the gap between abstract abstract machines and abstract definitional interpreters (functional pearl). 2018. PACMPL. Wei, Decker, Rompf https://dx.doi.org/10.1145/3236800

An Internalist Approach to Correct-by-Construction Compilers. 2018. PPDP. Pardo, Gunther, Pagano, Viera https://dx.doi.org/10.1145/3236950.3236965

ALCHEMY: A Language and Compiler for Homomorphic Encryption Made easY. 2018. CCS. Crockett, Peikert , Sharp https://dx.doi.org/10.1145/3243734.3243828

Effect handlers for the masses. 2018. PACMPL. Brachthäuser, Schuster, Ostermann https://dx.doi.org/10.1145/3276481

Tensor Comprehensions: Framework-Agnostic High-Performance Machine Learning Abstractions. 2018. ArXiv. Vasilache, Zinenko, Theodoridis, Goyal, DeVito, Moses, Verdoolaege, Adams, Cohen https://arxiv.org/abs/1802.04730

A Compiler-Compiler for DSL Embedding. 2018. ArXiv. Shaikhha, Jovanovic, Koch https://arxiv.org/abs/1808.01344

Formalisation of a frame stack semantics for a Java-like language. 2018. ArXiv. Schubert, Chrzaszcz https://arxiv.org/abs/1808.05342

Implementing Algebraic Effects in C - "Monads for Free in C". 2017. APLAS. Leijen https://dx.doi.org/10.1007/978-3-319-71237-6_17

A simple library implementation of binary sessions. 2017. J Funct Program. Padovani https://dx.doi.org/10.1017/S0956796816000289

Interactive programming in Agda – Objects and graphical user interfaces. 2017. Journal of Functional Programming. Abel , Adelsberger, Setzer https://dx.doi.org/10.1017/S0956796816000319

Under-optimized smart contracts devour your money. 2017. SANER. Chen, Li, Luo, Zhang https://dx.doi.org/10.1109/SANER.2017.7884650

Beginner’s luck: a language for property-based generators. 2017. POPL. Lampropoulos, Gallois-Wong, Hritcu, Hughes, Pierce, Xia https://dx.doi.org/10.1145/3009837.3009868

Hypercollecting semantics and its application to static analysis of information flow. 2017. POPL. Assaf, Naumann , Signoles, Totel, Tronel https://dx.doi.org/10.1145/3009837.3009889

Do be do be do. 2017. POPL. Lindley, McBride, McLaughlin https://dx.doi.org/10.1145/3009837.3009897

Type-and-scope safe programs and their proofs. 2017. CPP. Allais, Chapman, McBride, McKinna https://dx.doi.org/10.1145/3018610.3018613

The next 700 syntactical models of type theory. 2017. CPP. Boulier, Pédrot, Tabareau https://dx.doi.org/10.1145/3018610.3018620

Control-Flow Integrity. 2017. CSUR. Burow, Carr, Brunthaler , Payer , Nash, Larsen, Franz https://dx.doi.org/10.1145/3054924

Abstracting definitional interpreters (functional pearl). 2017. Proc ACM Program Lang. Darais , Labich, Nguyen, Horn https://dx.doi.org/10.1145/3110256

Algebraic graphs with class (functional pearl). 2017. Haskell. Mokhov https://dx.doi.org/10.1145/3122955.3122956

Defunctionalisation as modular closure conversion. 2017. PPDP. Schöpp https://dx.doi.org/10.1145/3131851.3131868

Copattern matching and first-class observations in OCaml, with a macro. 2017. PPDP. Laforgue, Régis-Gianas https://dx.doi.org/10.1145/3131851.3131869

Nonmalleable Information Flow Control. 2017. CCS. Cecchetti, Myers, Arden https://dx.doi.org/10.1145/3133956.3134054

A principled approach to ornamentation in ML. 2017. PACMPL. Williams, Rémy https://dx.doi.org/10.1145/3158109

Profunctor Optics: Modular Data Accessors. 2017. Art Sci Eng Program. Pickering, Gibbons, Wu https://dx.doi.org/10.22152/programming-journal.org/2017/1/7

Matching Logic. 2017. Logical Methods in Computer Science. Rosu https://dx.doi.org/10.23638/LMCS-13(4:28)2017

Effects Without Monads: Non-determinism - Back to the Meta Language. 2017. ML/OCaml. Kiselyov https://dx.doi.org/10.4204/EPTCS.294.2

A Co-contextual Type Checker for Featherweight Java. 2017. ECOOP. Kuci, Erdweg , Bracevac, Bejleri, Mezini https://dx.doi.org/10.4230/LIPIcs.ECOOP.2017.18

Verification by Reduction to Functional Programs. 2017. . Blanc https://dx.doi.org/10.5075/epfl-thesis-7636

Macrofication: Refactoring by Reverse Macro Expansion. 2016. ESOP. Schuster, Disney, Flanagan https://dx.doi.org/10.1007/978-3-662-49498-1_25

Transfinite Step-Indexing: Decoupling Concrete and Logical Steps. 2016. ESOP. Svendsen, Sieczkowski , Birkedal https://dx.doi.org/10.1007/978-3-662-49498-1_28

Effects as sessions, sessions as effects. 2016. POPL. Orchard , Yoshida https://dx.doi.org/10.1145/2837614.2837634

Supermonads: one notion to bind them all. 2016. Haskell. Bracker, Nilsson https://dx.doi.org/10.1145/2976002.2976012

Gentrification gone too far? affordable 2nd-class values for fun and (co-)effect. 2016. . Osvald, Essertel, Wu, Alayón, Rompf https://dx.doi.org/10.1145/3022671.2984009

Intersections and Unions of Session Types. 2016. ITRS. Acay, Pfenning https://dx.doi.org/10.4204/EPTCS.242.3

Bayesian Statistics in Software Engineering: Practical Guide and Case Studies. 2016. ArXiv. Furia https://arxiv.org/abs/1608.06865

An Inductive Proof Method for Simulation-based Compiler Correctness. 2016. ArXiv. Schneider, Smolka, Hack https://arxiv.org/abs/1611.09606

Practical interruptible conversations: distributed dynamic verification with multiparty session types and Python. 2015. Formal Methods Syst Des. Demangeon, Honda, Hu, Neykova, Yoshida https://dx.doi.org/10.1007/s10703-014-0218-8

Synchronizing namespaces with invertible bloom filters. 2015. ANCS. Fu, Abraham, Crowley https://dx.doi.org/10.1109/ANCS.2015.7110126

The Next 700 BFT Protocols. 2015. TOCS. Aublin, Guerraoui , Knezevic, Quéma, Vukolic https://dx.doi.org/10.1145/2658994

The Design of Terra: Harnessing the Best Features of High-Level and Low-Level Languages. 2015. SNAPL. DeVito, Hanrahan https://dx.doi.org/10.4230/LIPIcs.SNAPL.2015.79

Logical Physical Clocks. 2014. OPODIS. Kulkarni, Demirbas , Madappa, Avva, Leone https://dx.doi.org/10.1007/978-3-319-14472-6_2

Implicit Staging of EDSL Expressions: A Bridge between Shallow and Deep Embedding. 2014. ECOOP. Scherr, Chiba https://dx.doi.org/10.1007/978-3-662-44202-9_16

Pabble: parameterised Scribble. 2014. Service Oriented Computing and Applications. Ng, Yoshida https://dx.doi.org/10.1007/s11761-014-0172-8

How to keep your neighbours in order. 2014. ICFP. McBride https://dx.doi.org/10.1145/2628136.2628163

LiquidHaskell: experience with refinement types in the real world. 2014. Haskell. Vazou , Seidel, Jhala https://dx.doi.org/10.1145/2633357.2633366

SciFe: Scala framework for efficient enumeration of data structures with invariants. 2014. SCALA@ECOOP. Kuraj, Kuncak https://dx.doi.org/10.1145/2637647.2637655

Koka: Programming with Row Polymorphic Effect Types. 2014. MSFP. Leijen https://dx.doi.org/10.4204/EPTCS.153.8

Proving Termination Starting from the End. 2013. CAV. Ganty, Genaim https://dx.doi.org/10.1007/978-3-642-39799-8_27

Let’s ChronoSync: Decentralized dataset state synchronization in Named Data Networking. 2013. ICNP. Zhu, Afanasyev https://dx.doi.org/10.1109/ICNP.2013.6733578

Deadlock-freedom-by-design: multiparty asynchronous global programming. 2013. POPL. Carbone, Montesi https://dx.doi.org/10.1145/2429069.2429101

Multiparty Session C: Safe Parallel Programming with Message Optimisation. 2012. TOOLS. Ng, Yoshida, Honda https://dx.doi.org/10.1007/978-3-642-30561-0_15

Functorial data migration. 2012. Inf Comput. Spivak https://dx.doi.org/10.1016/j.ic.2012.05.001

Efficient state merging in symbolic execution. 2012. PLDI. Kuznetsov, Kinder, Bucur, Candea https://dx.doi.org/10.1145/2254064.2254088

Transporting functions across ornaments. 2012. ICFP. Dagand, McBride https://dx.doi.org/10.1145/2364527.2364544

Quorum Systems towards an Asynchronous Communication in Cognitive Radio Networks. 2012. J Electr Comput Eng. Romaszko, Mähönen https://dx.doi.org/10.1155/2012/753541

Quorum Systems: With Applications to Storage and Consensus. 2012. Synthesis Lectures on Distributed Computing Theory. Vukolic https://dx.doi.org/10.2200/S00402ED1V01Y201202DCT009

Compositionality Entails Sequentializability. 2011. TACAS. Garg, Madhusudan https://dx.doi.org/10.1007/978-3-642-19835-9_4

On the Nature of Progress. 2011. OPODIS. Herlihy, Shavit https://dx.doi.org/10.1007/978-3-642-25873-2_22

Testing an optimising compiler by generating random lambda terms. 2011. AST. Palka, Claessen, Russo, Hughes https://dx.doi.org/10.1145/1982595.1982615

On the nature of progress. 2011. . Lipari, Roy https://dx.doi.org/10.4135/9788132108177.n9

Type Preservation as a Confluence Problem. 2011. RTA. Stump, Kimmell, Omar https://dx.doi.org/10.4230/LIPIcs.RTA.2011.345

The Polyhedral Model Is More Widely Applicable Than You Think. 2010. CC. Benabderrahmane, Pouchet, Cohen, Bastoul https://dx.doi.org/10.1007/978-3-642-11970-5_16

A Survey of Symbolic Methods in Computational Analysis of Cryptographic Systems. 2010. Journal of Automated Reasoning. Cortier, Kremer, Warinschi https://dx.doi.org/10.1007/s10817-010-9187-9

Resolving and exploiting the k-CFA paradox: illuminating functional vs. object-oriented program analysis. 2010. PLDI. Might, Smaragdakis, Horn https://dx.doi.org/10.1145/1806596.1806631

Implementing first-class polymorphic delimited continuations by a type-directed selective CPS-transform. 2009. ICFP. Rompf , Maier, Odersky https://dx.doi.org/10.1145/1596550.1596596

An Equivalence Between Zero Knowledge and Commitments. 2008. TCC. Ong, Vadhan https://dx.doi.org/10.1007/978-3-540-78524-8_27

Engineering formal metatheory. 2008. POPL. Aydemir, Charguéraud, Pierce, Pollack, Weirich https://dx.doi.org/10.1145/1328438.1328443

Cryptographically sound implementations for typed information-flow security. 2008. . FournetCédric, RezkTamara https://dx.doi.org/10.1145/1328897.1328478

Typed closure conversion preserves observational equivalence. 2008. ICFP. Ahmed, Blume https://dx.doi.org/10.1145/1411204.1411227

Haskell session types with (almost) no class. 2008. Haskell. Pucella, Tov https://dx.doi.org/10.1145/1411286.1411290

Dynamic Logic. 2007. The KeY Approach. Beckert, Klebanov, Schlager https://dx.doi.org/10.1007/978-3-540-69061-0_3

Zero Knowledge and Soundness Are Symmetric. 2007. EUROCRYPT. Ong, Vadhan https://dx.doi.org/10.1007/978-3-540-72540-4_11

A Head-to-Head Comparison of de Bruijn Indices and Names. 2007. Electron Notes Theor Comput Sci. Berghofer, Urban https://dx.doi.org/10.1016/j.entcs.2007.01.018

A semantics for concurrent separation logic. 2007. Theor Comput Sci. Brookes https://dx.doi.org/10.1016/j.tcs.2006.12.034

Theorem proving support in programming language semantics. 2007. ArXiv. Bertot https://dx.doi.org/10.1017/CBO9780511770524.016

Acute: High-level programming language design for distributed computation. 2007. Journal of Functional Programming. Sewell , Leifer, Wansbrough, Nardelli, Allen-Williams, Habouzit, Vafeiadis https://dx.doi.org/10.1017/S0956796807006442

Concurrent programming without locks. 2007. TOCS. Fraser, Harris https://dx.doi.org/10.1145/1233307.1233309

A certified type-preserving compiler from lambda calculus to assembly language. 2007. PLDI. Chlipala https://dx.doi.org/10.1145/1250734.1250742

Formalizing and verifying semantic type soundness of a simple compiler. 2007. PPDP. Benton, Zarfaty https://dx.doi.org/10.1145/1273920.1273922

Links: Web Programming Without Tiers. 2006. FMCO. Cooper, Lindley, Wadler , Yallop https://dx.doi.org/10.1007/978-3-540-74792-5_12

Formal Semantics of Programming Languages: - An Overview -. 2006. Electron Notes Theor Comput Sci. Mosses https://dx.doi.org/10.1016/j.entcs.2005.12.012

Making a fast curry: push/enter vs. eval/apply for higher-order languages. 2006. J Funct Program. Marlow, Jones https://dx.doi.org/10.1017/S0956796806005995

History and Future of Implicit and Inductionless Induction: Beware the Old Jade and the Zombie!. 2005. Mechanizing Mathematical Reasoning. Wirth https://dx.doi.org/10.1007/978-3-540-32254-2_12

A functional correspondence between monadic evaluators and abstract machines for languages with computational effects. 2005. Theor Comput Sci. Ager, Danvy, Midtgaard https://dx.doi.org/10.1016/j.tcs.2005.06.008

End-to-end availability policies and noninterference. 2005. CSFW. Zheng, Myers https://dx.doi.org/10.1109/CSFW.2005.16

From sequential programs to multi-tier applications by program transformation. 2005. POPL. Neubauer, Thiemann https://dx.doi.org/10.1145/1040305.1040324

CUTE: a concolic unit testing engine for C. 2005. ESEC/FSE-. Sen, Marinov, Agha https://dx.doi.org/10.1145/1081706.1081750

Continuations and Web Servers. 2004. High Order Symb Comput. Queinnec https://dx.doi.org/10.1007/s10990-004-4866-z

Safety of abstract interpretations for free, via logical relations and Galois connections. 2004. Sci Comput Program. Backhouse, Backhouse https://dx.doi.org/10.1016/j.scico.2003.06.002

The view from the left. 2004. J Funct Program. McBride, McKinna https://dx.doi.org/10.1017/S0956796803004829

Propositions as Types. 2004. J Log Comput. Awodey, Bauer https://dx.doi.org/10.1093/logcom/14.4.447

A symmetric modal lambda calculus for distributed computing. 2004. LICS. Murphy, Crary , Harper, Pfenning https://dx.doi.org/10.1109/LICS.2004.7

Code Generation in the Polyhedral Model Is Easier Than You Think. 2004. IEEE PACT. Bastoul https://dx.doi.org/10.1109/PACT.2004.10018

Scalable and dynamic quorum systems. 2003. PODC. Naor, Wieder https://dx.doi.org/10.1007/s00446-004-0114-3

Scrap your boilerplate: a practical design pattern for generic programming. 2003. TLDI. Lämmel , Jones https://dx.doi.org/10.1145/604174.604179

Constructive design of a hierarchy of semantics of a transition system by abstract interpretation. 2002. Theor Comput Sci. Cousot https://dx.doi.org/10.1016/S0304-3975(00)00313-3

Brewer’s conjecture and the feasibility of consistent, available, partition-tolerant web services. 2002. SIGA. Gilbert , Lynch https://dx.doi.org/10.1145/564585.564601

Secure program partitioning. 2002. TOCS. Zdancewic, Zheng, Nystrom , Myers https://dx.doi.org/10.1145/566340.566343

The power of two random choices: a survey of tech-niques and results. 2001. . Mitzenmacher, Richa, Sitaraman https://dx.doi.org/10.1007/978-1-4615-0013-1_9

Metacomputation-Based Compiler Architecture. 2000. MPC. Harrison, Kamin https://dx.doi.org/10.1007/10722010_14

Interactive Programs in Dependent Type Theory. 2000. CSL. Hancock, Setzer https://dx.doi.org/10.1007/3-540-44622-2_21

The influence of browsers on evaluators or, continuations to program web servers. 2000. ICFP. Queinnec https://dx.doi.org/10.1145/351240.351243

Composing contracts: an adventure in financial engineering (functional pearl). 2000. ICFP. Jones, Eber, Seward https://dx.doi.org/10.1145/351240.351267

A new approach to abstract syntax involving binders. 1999. Cat No PR. Gabbay, Pitts https://dx.doi.org/10.1109/LICS.1999.782617

Compiling standard ML to Java bytecodes. 1998. ICFP. Benton, Kennedy, Russell https://dx.doi.org/10.1145/289423.289435

Two new quorum based algorithms for distributed mutual exclusion. 1997. Proceedings of th International Conference on Distributed Computing Systems. Luk, Wong https://dx.doi.org/10.1109/ICDCS.1997.597862

Multi-stage programming with explicit annotations. 1997. PEPM. Taha, Sheard https://dx.doi.org/10.1145/258993.259019

Types as abstract interpretations. 1997. POPL. Cousot https://dx.doi.org/10.1145/263699.263744

Abstract Compilation: A New Implementation Paradigm for Static Analysis. 1996. CC. Boucher, Feeley https://dx.doi.org/10.1007/3-540-61053-7_62

Reasoning with Executable Specifications. 1995. TAPSOFT. Bertot, Fraer https://dx.doi.org/10.1007/3-540-59293-8_218

A Syntactic Approach to Type Soundness. 1994. Inf Comput. Wright, Felleisen https://dx.doi.org/10.1006/inco.1994.1093

Global Flow Analysis as a Practical Compilation Tool. 1992. J Log Program. Hermenegildo , Warren, Debray https://dx.doi.org/10.1016/0743-1066(92)90053-6

Concerning the Size of Logical Clocks in Distributed Systems. 1991. Inf Process Lett. Charron-Bost https://dx.doi.org/10.1016/0020-0190(91)90055-M

Declarative Continuations: an Investigation of Duality in Programming Language Semantics. 1989. Category Theory and Computer Science. Filinski https://dx.doi.org/10.1007/BFb0018355

Natural Semantics. 1987. STACS. Kahn https://dx.doi.org/10.1007/BFb0039592

An approach to incremental compilation. 1984. SIGPLAN. Reiss https://dx.doi.org/10.1145/502874.502889

Coin flipping by telephone a protocol for solving impossible problems. 1983. SIGA. Blum https://dx.doi.org/10.1145/1008908.1008911

Impossibility of distributed consensus with one faulty process. 1983. PODS. Fischer , Lynch , Paterson https://dx.doi.org/10.1145/588058.588060

Domains for Denotational Semantics. 1982. ICALP. Scott https://dx.doi.org/10.1007/BFb0012801

A Theory of Type Polymorphism in Programming. 1978. J Comput Syst Sci. Milner https://dx.doi.org/10.1016/0022-0000(78)90014-4

Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. 1977. POPL. Cousot , Cousot https://dx.doi.org/10.1145/512950.512973

The denotational semantics of programming languages. 1976. CACM. Tennent https://dx.doi.org/10.1145/360303.360308

Definitional interpreters for higher-order programming languages. 1972. ACM. Reynolds https://dx.doi.org/10.1145/800194.805852

An axiomatic basis for computer programming. 1969. CACM. Hoare https://dx.doi.org/10.1145/363235.363259

CORRECTNESS OF A COMPILER FOR ARITHMETIC EXPRESSIONS. 1966. . McCarthy, Painter https://dx.doi.org/10.1090/psapm/019/0242403