Programming Languages

Authors and titles for January 2020

[1] arXiv:2001.01337 [pdf, other]

Title: A Diagrammatic Calculus for Algebraic Effects

Ugo Dal Lago, Francesco Gavazzo

Subjects: Programming Languages (cs.PL); Logic in Computer Science (cs.LO)

[2] arXiv:2001.02031 [pdf, other]

Title: Retentive Lenses

Zirun Zhu, Zhixuan Yang, Hsiang-Shang Ko, Zhenjiang Hu

Comments: 34 pages, 12 figures

Subjects: Programming Languages (cs.PL)

[3] arXiv:2001.02209 [pdf, other]

Title: Correctness of Automatic Differentiation via Diffeologies and Categorical Gluing

Mathieu Huot, Sam Staton, Matthijs Vákár

Comments: Proceedings of FoSSaCS 2020

Subjects: Programming Languages (cs.PL); Logic in Computer Science (cs.LO)

[4] arXiv:2001.02545 [pdf, other]

Title: Deep Static Modeling of invokedynamic

George Fourtounis, Yannis Smaragdakis

Journal-ref: ECOOP 2019

Subjects: Programming Languages (cs.PL)

[5] arXiv:2001.02630 [pdf, other]

Title: Albert, an intermediate smart-contract language for the Tezos blockchain

Bruno Bernardo, Raphaël Cauderlier, Basile Pesin, Julien Tesson

Comments: 15 pages. arXiv admin note: text overlap with arXiv:1909.08671

Subjects: Programming Languages (cs.PL)

[6] arXiv:2001.02659 [pdf, other]

Title: An Equational Theory for Weak Bisimulation via Generalized Parameterized Coinduction

Yannick Zakowski, Paul He, Chung-Kil Hur, Steve Zdancewic

Comments: To be published in CPP 2020

Subjects: Programming Languages (cs.PL); Logic in Computer Science (cs.LO)

[7] arXiv:2001.02828 [pdf, other]

Title: Monotone recursive types and recursive data representations in Cedille

Christopher Jenkins, Aaron Stump

Journal-ref: Math. Struct. Comp. Sci. 31 (2021) 682-745

Subjects: Programming Languages (cs.PL); Logic in Computer Science (cs.LO)

[8] arXiv:2001.02981 [pdf, other]

Title: Automatic generation and verification of test-stable floating-point code

Laura Titolo, Mariano Moscato, Cesar A. Muñoz

Comments: 32 pages. arXiv admin note: text overlap with arXiv:1808.04289

Subjects: Programming Languages (cs.PL); Numerical Analysis (math.NA)

[9] arXiv:2001.03256 [pdf, other]

Title: SMT-Friendly Formalization of the Solidity Memory Model

Ákos Hajdu, Dejan Jovanović

Comments: Authors' manuscript. Published in P. Müller (Ed.): ESOP 2020, LNCS 12075, 2020. The final publication is available at Springer via this https URL

Subjects: Programming Languages (cs.PL); Logic in Computer Science (cs.LO); Software Engineering (cs.SE)

[10] arXiv:2001.03541 [pdf, other]

Title: Multi-layer Optimizations for End-to-End Data Analytics

Amir Shaikhha, Maximilian Schleich, Alexandru Ghita, Dan Olteanu

Subjects: Programming Languages (cs.PL); Databases (cs.DB); Machine Learning (cs.LG)

[11] arXiv:2001.04301 [pdf, other]

Title: Tabled Typeclass Resolution

Daniel Selsam, Sebastian Ullrich, Leonardo de Moura

Subjects: Programming Languages (cs.PL); Logic in Computer Science (cs.LO)

[12] arXiv:2001.04439 [pdf, other]

Title: Session Types with Arithmetic Refinements and Their Application to Work Analysis

Ankush Das, Frank Pfenning

Subjects: Programming Languages (cs.PL); Logic in Computer Science (cs.LO)

[13] arXiv:2001.04961 [pdf, other]

Title: Atomicity Checking in Linear Time using Vector Clocks

Umang Mathur, Mahesh Viswanathan

Subjects: Programming Languages (cs.PL); Software Engineering (cs.SE)

[14] arXiv:2001.05059 [pdf, other]

Title: Gillian: Compositional Symbolic Execution for All

José Fragoso Santos, Petar Maksimović, Sacha-Élie Ayoun, Philippa Gardner

Subjects: Programming Languages (cs.PL); Logic in Computer Science (cs.LO)

[15] arXiv:2001.06163 [pdf, other]

Title: Proceedings 16th Workshop on Quantitative Aspects of Programming Languages and Systems

Alessandro Aldini (University of Urbino), Herbert Wiklicky (Imperial College London)

Journal-ref: EPTCS 312, 2020

Subjects: Programming Languages (cs.PL); Computer Science and Game Theory (cs.GT); Information Theory (cs.IT); Logic in Computer Science (cs.LO)

[16] arXiv:2001.06942 [pdf, other]

Title: Quantitative Aspects of Programming Languages and Systems over the past $2^4$ years and beyond

Alessandro Aldini (University of Urbino)

Comments: In Proceedings QAPL 2019, arXiv:2001.06163

Journal-ref: EPTCS 312, 2020, pp. 1-19

Subjects: Programming Languages (cs.PL); Information Theory (cs.IT); Logic in Computer Science (cs.LO)

[17] arXiv:2001.06943 [pdf, other]

Title: Probabilistic Output Analyses for Deterministic Programs --- Reusing Existing Non-probabilistic Analyses

Maja Hanne Kirkeby (Computer Science, Roskilde University, Denmark)

Comments: In Proceedings QAPL 2019, arXiv:2001.06163

Journal-ref: EPTCS 312, 2020, pp. 43-57

Subjects: Programming Languages (cs.PL)

[18] arXiv:2001.07488 [pdf, other]

Title: Profunctor Optics, a Categorical Update

Bryce Clarke, Derek Elkins, Jeremy Gibbons, Fosco Loregian, Bartosz Milewski, Emily Pillmore, Mario Román

Comments: 38 pages. Final version with Compositionality metadata, does not change theorem numbering

Journal-ref: Compositionality, Volume 6 (2024) (February 23, 2024) compositionality:13530

Subjects: Programming Languages (cs.PL); Category Theory (math.CT)

[19] arXiv:2001.08045 [pdf, other]

Title: Profunctor optics and traversals

Mario Román

Comments: Submitted as a thesis for MSc Mathematics and Foundations of Computer Science, University of Oxford 2019. The work on the article "Profunctor optics, a categorical update" started in this MSc dissertation. 82 pages

Subjects: Programming Languages (cs.PL); Category Theory (math.CT)

[20] arXiv:2001.08133 [pdf, other]

Title: Drawing Prolog Search Trees: A Manual for Teachers and Students of Logic Programming

Johan Bos

Comments: 20 pages, 8 listings, 7 figures

Subjects: Programming Languages (cs.PL); Logic in Computer Science (cs.LO)

[21] arXiv:2001.10150 [pdf, other]

Title: Central Moment Analysis for Cost Accumulators in Probabilistic Programs

Di Wang, Jan Hoffmann, Thomas Reps

Subjects: Programming Languages (cs.PL)

[22] arXiv:2001.10274 [pdf, other]

Title: Unifying graded and parameterised monads

Dominic Orchard (University of Kent), Philip Wadler (University of Edinburgh), Harley Eades III (Augusta University)

Comments: In Proceedings MSFP 2020, arXiv:2004.14735

Journal-ref: EPTCS 317, 2020, pp. 18-38

Subjects: Programming Languages (cs.PL); Category Theory (math.CT)

[23] arXiv:2001.10328 [pdf, other]

Title: Verification of a Generative Separation Kernel

Inzemamul Haque, Deepak D'Souza, Habeeb P, Arnab Kundu, Ganesh Babu

Subjects: Programming Languages (cs.PL)

[24] arXiv:2001.10490 [pdf, other]

Title: Beyond Notations: Hygienic Macro Expansion for Theorem Proving Languages

Sebastian Ullrich, Leonardo de Moura

Journal-ref: Logical Methods in Computer Science, Volume 18, Issue 2 (April 13, 2022) lmcs:7421

Subjects: Programming Languages (cs.PL)

[25] arXiv:2001.10594 [pdf, other]

Title: Simplifying Casts and Coercions

Robert Y. Lewis, Paul-Nicolas Madelaine

Subjects: Programming Languages (cs.PL)

[26] arXiv:2001.10723 [pdf, other]

Title: Concise Read-Only Specifications for Better Synthesis of Programs with Pointers -- Extended Version

Andreea Costea, Amy Zhu, Nadia Polikarpova, Ilya Sergey

Subjects: Programming Languages (cs.PL); Logic in Computer Science (cs.LO)

[27] arXiv:2001.11001 [pdf, other]

Title: A Type and Scope Safe Universe of Syntaxes with Binding: Their Semantics and Proofs

Guillaume Allais, Robert Atkey, James Chapman, Conor McBride, James McKinna

Comments: Extended version of the ICFP 18 paper

Subjects: Programming Languages (cs.PL)

[28] arXiv:2001.11560 [pdf, other]

Title: Parameterized Cast Calculi and Reusable Meta-theory for Gradually Typed Lambda Calculi

Jeremy G. Siek

Comments: In submission to Journal of Functional Programming

Subjects: Programming Languages (cs.PL)

[29] arXiv:2001.11604 [pdf, other]

Title: Diva: A Declarative and Reactive Language for In-Situ Visualization

Qi Wu (1), Tyson Neuroth (1), Oleg Igouchkine (1), Konduri Aditya (2), Jacqueline H. Chen (3), Kwan-Liu Ma (1) ((1) UC Davis, (2) Indian Institute of Science, (3) Sandia National Laboratories)

Comments: 11 pages, 5 figures, 6 listings, 1 table, to be published in LDAV 2020. The article has gone through 2 major revisions: Emphasized contributions, features and examples. Addressed connections between DIVA and FRP. In sec. 3, we fixed a design flaw and addressed it in sec. 3.3-3.4. Re-designed sec. 5 with a more concrete example and benchmark results. Simplified the syntax of DIVA

Subjects: Programming Languages (cs.PL); Human-Computer Interaction (cs.HC)

[30] arXiv:2001.11816 [pdf, other]

Title: Understanding Profunctor Optics: a representation theorem

Guillaume Boisseau

Comments: Submitted as a thesis for the degree of MSc in Computer Science at the University of Oxford in 2017. 65 pages

Subjects: Programming Languages (cs.PL)

[31] arXiv:2001.11819 [pdf, other]

Title: Joint Distributions for TensorFlow Probability

Dan Piponi, Dave Moore, Joshua V. Dillon

Comments: Based on extended abstract submitted to PROBPROG 2020

Subjects: Programming Languages (cs.PL); Machine Learning (cs.LG); Computation (stat.CO); Machine Learning (stat.ML)

[32] arXiv:2001.00059 (cross-list from cs.SE) [pdf, other]

Title: Learning and Evaluating Contextual Embedding of Source Code

Aditya Kanade, Petros Maniatis, Gogul Balakrishnan, Kensen Shi

Comments: Published in ICML 2020. This version (v.3) is the final camera-ready version of the paper. It contains the re-computed results, based on the open-sourced datasets

Subjects: Software Engineering (cs.SE); Computation and Language (cs.CL); Machine Learning (cs.LG); Programming Languages (cs.PL)

[33] arXiv:2001.00532 (cross-list from cs.MS) [pdf, other]

Title: A Unified Iteration Space Transformation Framework for Sparse and Dense Tensor Algebra

Ryan Senanayake, Fredrik Kjolstad, Changwan Hong, Shoaib Kamil, Saman Amarasinghe

Subjects: Mathematical Software (cs.MS); Programming Languages (cs.PL)

[34] arXiv:2001.00806 (cross-list from cs.CR) [pdf, other]

Title: Verifying Cryptographic Security Implementations in C Using Automated Model Extraction

Mihhail Aizatulin

Subjects: Cryptography and Security (cs.CR); Programming Languages (cs.PL)

[35] arXiv:2001.01516 (cross-list from cs.LO) [pdf, other]

Title: A Calculus for Modular Loop Acceleration

Florian Frohn

Subjects: Logic in Computer Science (cs.LO); Programming Languages (cs.PL)

[36] arXiv:2001.02609 (cross-list from cs.MS) [pdf, other]

Title: Automatic Generation of Efficient Sparse Tensor Format Conversion Routines

Stephen Chou, Fredrik Kjolstad, Saman Amarasinghe

Comments: Presented at PLDI 2020

Subjects: Mathematical Software (cs.MS); Programming Languages (cs.PL)

[37] arXiv:2001.02656 (cross-list from stat.ML) [pdf, other]

Title: Stochastic Probabilistic Programs

David Tolpin, Tomer Dobkin

Comments: 7 pages main body, 4 pages appendix

Subjects: Machine Learning (stat.ML); Machine Learning (cs.LG); Programming Languages (cs.PL)

[38] arXiv:2001.04729 (cross-list from math.OC) [pdf, other]

Title: A unified method to decentralized state inference and fault diagnosis/prediction of discrete-event systems

Kuize Zhang

Comments: 30 pages,12 figures, 2 tables

Subjects: Optimization and Control (math.OC); Programming Languages (cs.PL); Systems and Control (eess.SY)

[39] arXiv:2001.05132 (cross-list from cs.LO) [pdf, other]

Title: Strong Progress for Session-Typed Processes in a Linear Metalogic with Circular Proofs

Farzaneh Derakhshan, Frank Pfenning

Subjects: Logic in Computer Science (cs.LO); Programming Languages (cs.PL)

[40] arXiv:2001.06952 (cross-list from cs.FL) [pdf, other]

Title: Streaming Transformations of Infinite Ordered-Data Words

Xiaokang Qiu

Subjects: Formal Languages and Automata Theory (cs.FL); Logic in Computer Science (cs.LO); Programming Languages (cs.PL)

[41] arXiv:2001.07063 (cross-list from cs.LO) [pdf, other]

Title: Modular coinduction up-to for higher-order languages via first-order transition systems

Jean-Marie Madiot, Damien Pous, Davide Sangiorgi

Journal-ref: Logical Methods in Computer Science, Volume 17, Issue 3 (September 17, 2021) lmcs:6046

Subjects: Logic in Computer Science (cs.LO); Programming Languages (cs.PL)

[42] arXiv:2001.08040 (cross-list from cs.LO) [pdf, other]

Title: Axiomatizing Maximal Progress and Discrete Time

Mario Bravetti

Journal-ref: Logical Methods in Computer Science, Volume 17, Issue 1 (January 21, 2021) lmcs:6048

Subjects: Logic in Computer Science (cs.LO); Programming Languages (cs.PL)

[43] arXiv:2001.09258 (cross-list from cs.MS) [pdf, other]

Title: SLEEF: A Portable Vectorized Library of C Standard Mathematical Functions

Naoki Shibata, Francesco Petrogalli

Comments: in IEEE Transactions on Parallel and Distributed Systems. This is a version with all appendices included in a PDF. Accompanying software can be accessed at this https URL or this https URL

Subjects: Mathematical Software (cs.MS); Distributed, Parallel, and Cluster Computing (cs.DC); Programming Languages (cs.PL)

[44] arXiv:2001.09649 (cross-list from cs.LO) [pdf, other]

Title: Operationally-based Program Equivalence Proofs using LCTRSs

Ştefan Ciobâcă, Dorel Lucanu, Andrei Sebastian Buruiană

Subjects: Logic in Computer Science (cs.LO); Programming Languages (cs.PL)

[45] arXiv:2001.09995 (cross-list from cs.DC) [pdf, other]

Title: Automated Parallel Kernel Extraction from Dynamic Application Traces

Richard Uhrie, Chaitali Chakrabarti, John Brunhaver

Comments: 14 pages, 16 figures. Submitted to IEEE Transactions on Parallel and Distributed Systems

Subjects: Distributed, Parallel, and Cluster Computing (cs.DC); Programming Languages (cs.PL)

[46] arXiv:2001.10052 (cross-list from cs.SE) [pdf, other]

Title: SeMA: Extending and Analyzing Storyboards to Develop Secure Android Apps

Joydeep Mitra, Venkatesh-Prasad Ranganath, Torben Amtoft, Mike Higgins

Comments: Updates based on reviews MobileSoft, FSE, and Onward reviews. Added content about usability evaluation. Added formal syntax and semantics of the DSL and info flow analysis. Added acknowledgement

Subjects: Software Engineering (cs.SE); Cryptography and Security (cs.CR); Programming Languages (cs.PL)

[47] arXiv:2001.10630 (cross-list from cs.CR) [pdf, other]

Title: First-Order Logic for Flow-Limited Authorization

Andrew K. Hirsch, Pedro H. Azevedo de Amorim, Ethan Cecchetti, Ross Tate, Owen Arden

Comments: Coq code can be found at this https URL

Subjects: Cryptography and Security (cs.CR); Logic in Computer Science (cs.LO); Programming Languages (cs.PL)

[48] arXiv:2001.10799 (cross-list from cs.AI) [pdf, other]

Title: Business Negotiation Definition Language

Rustam Tagiew

Subjects: Artificial Intelligence (cs.AI); Formal Languages and Automata Theory (cs.FL); Logic in Computer Science (cs.LO); Programming Languages (cs.PL)

[49] arXiv:2001.10834 (cross-list from cs.AI) [pdf, other]

Title: Smart Induction for Isabelle/HOL (System Description)

Yutaka Nagashima

Comments: Under submission at IJCAR2020 as a System Description

Subjects: Artificial Intelligence (cs.AI); Logic in Computer Science (cs.LO); Programming Languages (cs.PL); Symbolic Computation (cs.SC)