kirancodes.me
To Proof Maintenance & Beyond!
Venues / JFP /

JFP 2021

31 papers

  1. A greedy algorithm for dropping digits · Richard S. Bird, Shin-Cheng Mu
  2. A trustful monad for axiomatic reasoning with probability and nondeterminism · Reynald Affeldt, Jacques Garrigue, David Nowak, Takafumi Saikawa
  3. A type- and scope-safe universe of syntaxes with binding: their semantics and proofs · Guillaume Allais, Robert Atkey, James Chapman, Conor McBride, James McKinna
  4. Blame and coercion: Together again for the first time · Jeremy G. Siek, Peter Thiemann, Philip Wadler
  5. Cogent: uniqueness types and certifying compilation · Liam O'Connor, Zilin Chen, Christine Rizkallah, Vincent Jackson, Sidney Amani, Gerwin Klein + 3 more
  6. Composable data visualizations · Tomas Petricek
  7. Cubical Agda: A dependently typed programming language with univalence and higher inductive types · Andrea Vezzosi, Anders Mörtberg, Andreas Abel
  8. Explainable dynamic programming · Martin Erwig, Prashant Kumar
  9. Extensional equality preservation and verified generic programming · Nicola Botta, Nuria Brede, Patrik Jansson, Tim Richter
  10. Gradual type theory · Max S. New, Daniel R. Licata, Amal Ahmed
  11. Higher order functions and Brouwer's thesis · Jonathan Sterling
  12. How to design co-programs · Jeremy Gibbons
  13. Integrating region memory management and tag-free generational garbage collection · Martin Elsman, Niels Hallenberg
  14. Lambda calculus with algebraic simplification for reduction parallelisation: Extended study · Akimasa Morihata
  15. Linear capabilities for fully abstract compilation of separation-logic-verified code · Thomas Van Strydonck, Frank Piessens, Dominique Devriese
  16. Longest segment of balanced parentheses: an exercise in program inversion in a segment problem · Shin-Cheng Mu, Tsung-Ju Chiang
  17. Not by equations alone: Reasoning with extensible effects · Oleg Kiselyov, Shin-Cheng Mu, Amr Sabry
  18. On the correctness of monadic backward induction · Nuria Brede, Nicola Botta
  19. Parameterized cast calculi and reusable meta-theory for gradually typed lambda calculi · Jeremy G. Siek, Tianyu Chen
  20. PhD Abstracts · Graham Hutton
  21. PhD Abstracts · Graham Hutton
  22. Proof-directed program transformation: A functional account of efficient regular expression matching · Andrzej Filinski
  23. Protocol combinators for modeling, testing, and execution of distributed systems · Kristoffer Just Arndal Andersen, Ilya Sergey
  24. Ready, Set, Verify! Applying hs-to-coq to real-world Haskell code · Joachim Breitner, Antal Spector-Zabusky, Yao Li, Christine Rizkallah, John Wiegley, Joshua M. Cohen + 1 more
  25. Real-time MLton: A Standard ML runtime for real-time functional programs · Bhargav Shivkumar, Jeffrey C. Murphy, Lukasz Ziarek
  26. Relational cost analysis in a functional-imperative setting · Weihao Qu, Marco Gaboardi, Deepak Garg
  27. Segments: An alternative rainfall problem · Peter Achten
  28. StkTokens: Enforcing well-bracketed control flow and stack encapsulation using linear capabilities · Lau Skorstengaard, Dominique Devriese, Lars Birkedal
  29. Taming the Merge Operator · Xuejing Huang, Jinxu Zhao, Bruno C. d. S. Oliveira
  30. Verified secure compilation for mixed-sensitivity concurrent programs · Robert Sison, Toby Murray
  31. What is an education paper? · Shriram Krishnamurthi