Programming Languages

Authors and titles for January 2020

[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)