APLAS 2019

24 papers

1. A Dependently Typed Multi-stage Calculus · Akira Kawata, Atsushi Igarashi
2. A Type-Based HFL Model Checking Algorithm · Youkichi Hosoi, Naoki Kobayashi, Takeshi Tsukada
3. Android Multitasking Mechanism: Formal Semantics and Static Analysis of Apps · Jinlong He, Taolue Chen, Ping Wang, Zhilin Wu, Jun Yan
4. Completeness of Cyclic Proofs for Symbolic Heaps with Inductive Definitions · Makoto Tatsuta, Koji Nakazawa, Daisuke Kimura
5. Compositional Verification of Heap-Manipulating Programs Through Property-Guided Learning · Long H. Pham, Jun Sun, Quang Loc Le
6. Conflict Abstractions and Shadow Speculation for Optimistic Transactional Objects · Thomas D. Dickerson, Eric Koskinen, Paul Gazzillo, Maurice Herlihy
7. Dissecting Widening: Separating Termination from Information · Graeme Gange, Jorge A. Navas, Peter Schachte, Harald Søndergaard, Peter J. Stuckey
8. Existential Types for Relaxed Noninterference · Raimil Cruz, Éric Tanter
9. Factorization and Normalization, Essentially · Beniamino Accattoli, Claudia Faggian, Giulio Guerrieri
10. Formal Verifications of Call-by-Need and Call-by-Name Evaluations with Mutual Recursion · Masayuki Mizuno, Eijiro Sumii
11. J-ReCoVer: Java Reducer Commutativity Verifier · Yu-Fang Chen, Chang-Yi Chiang, Lukás Holík, Wei-Tsung Kao, Hsin-Hung Lin, Tomás Vojnar + 2 more
12. LiFtEr: Language to Encode Induction Heuristics for Isabelle/HOL · Yutaka Nagashima
13. Lightweight Functional Logic Meta-Programming · Nada Amin, William E. Byrd, Tiark Rompf
14. Manifest Contracts with Intersection Types · Yuki Nishida, Atsushi Igarashi
15. Mimalloc: Free List Sharding in Action · Daan Leijen, Benjamin Zorn, Leonardo de Moura
16. On Strings in Software Model Checking · Hossein Hojjat, Philipp Rümmer, Ali Shamakhi
17. Proving that Programs Are Differentially Private · Annabelle McIver, Carroll Morgan
18. Pumping, with or Without Choice · Aquinas Hobor, Elaine Li, Frank Stephan
19. Recursion Schemes in Coq · Kosuke Murata, Kento Emoto
20. Reducing Static Analysis Alarms Based on Non-impacting Control Dependencies · Tukaram Muske, Rohith Talluri, Alexander Serebrenik
21. Simulations in Rank-Based Büchi Automata Complementation · Yu-Fang Chen, Vojtech Havlena, Ondrej Lengál
22. Succinct Determinisation of Counting Automata via Sphere Construction · Lukás Holík, Ondrej Lengál, Olli Saarikivi, Lenka Turonová, Margus Veanes, Tomás Vojnar
23. TxForest: A DSL for Concurrent Filestores · Jonathan DiLorenzo, Katie Mancini, Kathleen Fisher, Nate Foster
24. Uniform Random Process Model Revisited · Wenbo Zhang, Huan Long, Xian Xu