Workshop MAPL 2017 – Author Index 
Contents 
Abstracts 
Authors

Abadi, Martín 
MAPL '17: "A Computational Model for ..."
A Computational Model for TensorFlow: An Introduction
Martín Abadi, Michael Isard, and Derek G. Murray (Google Brain, USA) TensorFlow is a powerful, programmable system for machine learning. This paper aims to provide the basics of a conceptual framework for understanding the behavior of TensorFlow models during training and inference: it describes an operational semantics, of the kind common in the literature on programming languages. More broadly, the paper suggests that a programminglanguage perspective is fruitful in designing and in explaining systems such as TensorFlow. @InProceedings{MAPL17p1, author = {Martín Abadi and Michael Isard and Derek G. Murray}, title = {A Computational Model for TensorFlow: An Introduction}, booktitle = {Proc.\ MAPL}, publisher = {ACM}, pages = {17}, doi = {10.1145/3088525.3088527}, year = {2017}, } Publisher's Version Article Search 

Eisner, Jason 
MAPL '17: "Dyna: Toward a SelfOptimizing ..."
Dyna: Toward a SelfOptimizing Declarative Language for Machine Learning Applications
Tim Vieira, Matthew FrancisLandau, Nathaniel Wesley Filardo, Farzad Khorasani, and Jason Eisner (Johns Hopkins University, USA; Rice University, USA) Declarative programming is a paradigm that allows programmers to specify what they want to compute, leaving how to compute it to a solver. Our declarative programming language, Dyna, is designed to compactly specify computations like those that are frequently encountered in machine learning. As a declarative language, Dyna’s solver has a large space of (correct) strategies available to it. We describe a reinforcement learning framework for adaptively choosing among these strategies to maximize efficiency for a given workload. Adaptivity in execution is especially important for software that will run under a variety of workloads, where no fixed policy works well. We hope that reinforcement learning will identify good policies reasonably quickly—offloading the burden of writing efficient code from human programmers. @InProceedings{MAPL17p8, author = {Tim Vieira and Matthew FrancisLandau and Nathaniel Wesley Filardo and Farzad Khorasani and Jason Eisner}, title = {Dyna: Toward a SelfOptimizing Declarative Language for Machine Learning Applications}, booktitle = {Proc.\ MAPL}, publisher = {ACM}, pages = {817}, doi = {10.1145/3088525.3088562}, year = {2017}, } Publisher's Version Article Search 

Filardo, Nathaniel Wesley 
MAPL '17: "Dyna: Toward a SelfOptimizing ..."
Dyna: Toward a SelfOptimizing Declarative Language for Machine Learning Applications
Tim Vieira, Matthew FrancisLandau, Nathaniel Wesley Filardo, Farzad Khorasani, and Jason Eisner (Johns Hopkins University, USA; Rice University, USA) Declarative programming is a paradigm that allows programmers to specify what they want to compute, leaving how to compute it to a solver. Our declarative programming language, Dyna, is designed to compactly specify computations like those that are frequently encountered in machine learning. As a declarative language, Dyna’s solver has a large space of (correct) strategies available to it. We describe a reinforcement learning framework for adaptively choosing among these strategies to maximize efficiency for a given workload. Adaptivity in execution is especially important for software that will run under a variety of workloads, where no fixed policy works well. We hope that reinforcement learning will identify good policies reasonably quickly—offloading the burden of writing efficient code from human programmers. @InProceedings{MAPL17p8, author = {Tim Vieira and Matthew FrancisLandau and Nathaniel Wesley Filardo and Farzad Khorasani and Jason Eisner}, title = {Dyna: Toward a SelfOptimizing Declarative Language for Machine Learning Applications}, booktitle = {Proc.\ MAPL}, publisher = {ACM}, pages = {817}, doi = {10.1145/3088525.3088562}, year = {2017}, } Publisher's Version Article Search 

Foster, Jeffrey S. 
MAPL '17: "Learning a Classifier for ..."
Learning a Classifier for False Positive Error Reports Emitted by Static Code Analysis Tools
Ugur Koc, Parsa Saadatpanah, Jeffrey S. Foster, and Adam A. Porter (University of Maryland at College Park, USA) The large scale and high complexity of modern software systems make perfectly precise static code analysis (SCA) infeasible. Therefore SCA tools often overapproximate, so not to miss any real problems. This, however, comes at the expense of raising false alarms, which, in practice, reduces the usability of these tools. To partially address this problem, we propose a novel learning process whose goal is to discover program structures that cause a given SCA tool to emit false error reports, and then to use this information to predict whether a new error report is likely to be a false positive as well. To do this, we first preprocess code to isolate the locations that are related to the error report. Then, we apply machine learning techniques to the preprocessed code to discover correlations and to learn a classifier. We evaluated this approach in an initial case study of a widelyused SCA tool for Java. Our results showed that for our dataset we could accurately classify a large majority of false positive error reports. Moreover, we identified some common coding patterns that led to false positive errors. We believe that SCA developers may be able to redesign their methods to address these patterns and reduce false positive error reports. @InProceedings{MAPL17p35, author = {Ugur Koc and Parsa Saadatpanah and Jeffrey S. Foster and Adam A. Porter}, title = {Learning a Classifier for False Positive Error Reports Emitted by Static Code Analysis Tools}, booktitle = {Proc.\ MAPL}, publisher = {ACM}, pages = {3542}, doi = {10.1145/3088525.3088675}, year = {2017}, } Publisher's Version Article Search 

FrancisLandau, Matthew 
MAPL '17: "Dyna: Toward a SelfOptimizing ..."
Dyna: Toward a SelfOptimizing Declarative Language for Machine Learning Applications
Tim Vieira, Matthew FrancisLandau, Nathaniel Wesley Filardo, Farzad Khorasani, and Jason Eisner (Johns Hopkins University, USA; Rice University, USA) Declarative programming is a paradigm that allows programmers to specify what they want to compute, leaving how to compute it to a solver. Our declarative programming language, Dyna, is designed to compactly specify computations like those that are frequently encountered in machine learning. As a declarative language, Dyna’s solver has a large space of (correct) strategies available to it. We describe a reinforcement learning framework for adaptively choosing among these strategies to maximize efficiency for a given workload. Adaptivity in execution is especially important for software that will run under a variety of workloads, where no fixed policy works well. We hope that reinforcement learning will identify good policies reasonably quickly—offloading the burden of writing efficient code from human programmers. @InProceedings{MAPL17p8, author = {Tim Vieira and Matthew FrancisLandau and Nathaniel Wesley Filardo and Farzad Khorasani and Jason Eisner}, title = {Dyna: Toward a SelfOptimizing Declarative Language for Machine Learning Applications}, booktitle = {Proc.\ MAPL}, publisher = {ACM}, pages = {817}, doi = {10.1145/3088525.3088562}, year = {2017}, } Publisher's Version Article Search 

Gray, Patrick 
MAPL '17: "Verified Perceptron Convergence ..."
Verified Perceptron Convergence Theorem
Charlie Murphy, Patrick Gray, and Gordon Stewart (Princeton University, USA; Ohio University, USA) Frank Rosenblatt invented the perceptron algorithm in 1957 as part of an early attempt to build ``brain models'', artificial neural networks. In this paper, we apply tools from symbolic logic such as dependent type theory as implemented in Coq to build, and prove convergence of, onelayer perceptrons (specifically, we show that our Coq implementation converges to a binary classifier when trained on linearly separable datasets). Our perceptron and proof are extensible, which we demonstrate by adapting our convergence proof to the averaged perceptron, a common variant of the basic perceptron algorithm. We perform experiments to evaluate the performance of our Coq perceptron vs. an arbitraryprecision C++ implementation and against a hybrid implementation in which separators learned in C++ are certified in Coq. We find that by carefully optimizing the extraction of our Coq perceptron, we can meet  and occasionally exceed  the performance of the arbitraryprecision C++ implementation. Our hybrid Coq certifier demonstrates an architecture for building highassurance machinelearning systems that reuse existing codebases. @InProceedings{MAPL17p43, author = {Charlie Murphy and Patrick Gray and Gordon Stewart}, title = {Verified Perceptron Convergence Theorem}, booktitle = {Proc.\ MAPL}, publisher = {ACM}, pages = {4350}, doi = {10.1145/3088525.3088673}, year = {2017}, } Publisher's Version Article Search Info 

Grossman, Dan 
MAPL '17: "Debugging Probabilistic Programs ..."
Debugging Probabilistic Programs
Chandrakana Nandi, Dan Grossman, Adrian Sampson, Todd Mytkowicz, and Kathryn S. McKinley (University of Washington, USA; Cornell University, USA; Microsoft Research, USA; Google, USA) Many applications compute with estimated and uncertain data. While advances in probabilistic programming help developers build such applications, debugging them remains extremely challenging. New types of errors in probabilistic programs include 1) ignoring dependencies and correlation between random variables and in training data, 2) poorly chosen inference hyperparameters, and 3) incorrect statistical models. A partial solution to prevent these errors in some languages forbids developers from explicitly invoking inference. While this prevents some dependence errors, it limits composition and control over inference, and does not guarantee absence of other types of errors. This paper presents the FLEXI programming model which supports constructs for invoking inference in the language and reusing the results in other statistical computations. We define a novel formalism for inference with a Decorated Bayesian Network and present a tool, DePP, that analyzes this representation to identify the above errors. We evaluate DePP on a range of prototypical examples to show how it helps developers to detect errors. @InProceedings{MAPL17p18, author = {Chandrakana Nandi and Dan Grossman and Adrian Sampson and Todd Mytkowicz and Kathryn S. McKinley}, title = {Debugging Probabilistic Programs}, booktitle = {Proc.\ MAPL}, publisher = {ACM}, pages = {1826}, doi = {10.1145/3088525.3088564}, year = {2017}, } Publisher's Version Article Search 

Isard, Michael 
MAPL '17: "A Computational Model for ..."
A Computational Model for TensorFlow: An Introduction
Martín Abadi, Michael Isard, and Derek G. Murray (Google Brain, USA) TensorFlow is a powerful, programmable system for machine learning. This paper aims to provide the basics of a conceptual framework for understanding the behavior of TensorFlow models during training and inference: it describes an operational semantics, of the kind common in the literature on programming languages. More broadly, the paper suggests that a programminglanguage perspective is fruitful in designing and in explaining systems such as TensorFlow. @InProceedings{MAPL17p1, author = {Martín Abadi and Michael Isard and Derek G. Murray}, title = {A Computational Model for TensorFlow: An Introduction}, booktitle = {Proc.\ MAPL}, publisher = {ACM}, pages = {17}, doi = {10.1145/3088525.3088527}, year = {2017}, } Publisher's Version Article Search 

Khorasani, Farzad 
MAPL '17: "Dyna: Toward a SelfOptimizing ..."
Dyna: Toward a SelfOptimizing Declarative Language for Machine Learning Applications
Tim Vieira, Matthew FrancisLandau, Nathaniel Wesley Filardo, Farzad Khorasani, and Jason Eisner (Johns Hopkins University, USA; Rice University, USA) Declarative programming is a paradigm that allows programmers to specify what they want to compute, leaving how to compute it to a solver. Our declarative programming language, Dyna, is designed to compactly specify computations like those that are frequently encountered in machine learning. As a declarative language, Dyna’s solver has a large space of (correct) strategies available to it. We describe a reinforcement learning framework for adaptively choosing among these strategies to maximize efficiency for a given workload. Adaptivity in execution is especially important for software that will run under a variety of workloads, where no fixed policy works well. We hope that reinforcement learning will identify good policies reasonably quickly—offloading the burden of writing efficient code from human programmers. @InProceedings{MAPL17p8, author = {Tim Vieira and Matthew FrancisLandau and Nathaniel Wesley Filardo and Farzad Khorasani and Jason Eisner}, title = {Dyna: Toward a SelfOptimizing Declarative Language for Machine Learning Applications}, booktitle = {Proc.\ MAPL}, publisher = {ACM}, pages = {817}, doi = {10.1145/3088525.3088562}, year = {2017}, } Publisher's Version Article Search 

Koc, Ugur 
MAPL '17: "Learning a Classifier for ..."
Learning a Classifier for False Positive Error Reports Emitted by Static Code Analysis Tools
Ugur Koc, Parsa Saadatpanah, Jeffrey S. Foster, and Adam A. Porter (University of Maryland at College Park, USA) The large scale and high complexity of modern software systems make perfectly precise static code analysis (SCA) infeasible. Therefore SCA tools often overapproximate, so not to miss any real problems. This, however, comes at the expense of raising false alarms, which, in practice, reduces the usability of these tools. To partially address this problem, we propose a novel learning process whose goal is to discover program structures that cause a given SCA tool to emit false error reports, and then to use this information to predict whether a new error report is likely to be a false positive as well. To do this, we first preprocess code to isolate the locations that are related to the error report. Then, we apply machine learning techniques to the preprocessed code to discover correlations and to learn a classifier. We evaluated this approach in an initial case study of a widelyused SCA tool for Java. Our results showed that for our dataset we could accurately classify a large majority of false positive error reports. Moreover, we identified some common coding patterns that led to false positive errors. We believe that SCA developers may be able to redesign their methods to address these patterns and reduce false positive error reports. @InProceedings{MAPL17p35, author = {Ugur Koc and Parsa Saadatpanah and Jeffrey S. Foster and Adam A. Porter}, title = {Learning a Classifier for False Positive Error Reports Emitted by Static Code Analysis Tools}, booktitle = {Proc.\ MAPL}, publisher = {ACM}, pages = {3542}, doi = {10.1145/3088525.3088675}, year = {2017}, } Publisher's Version Article Search 

McKinley, Kathryn S. 
MAPL '17: "Debugging Probabilistic Programs ..."
Debugging Probabilistic Programs
Chandrakana Nandi, Dan Grossman, Adrian Sampson, Todd Mytkowicz, and Kathryn S. McKinley (University of Washington, USA; Cornell University, USA; Microsoft Research, USA; Google, USA) Many applications compute with estimated and uncertain data. While advances in probabilistic programming help developers build such applications, debugging them remains extremely challenging. New types of errors in probabilistic programs include 1) ignoring dependencies and correlation between random variables and in training data, 2) poorly chosen inference hyperparameters, and 3) incorrect statistical models. A partial solution to prevent these errors in some languages forbids developers from explicitly invoking inference. While this prevents some dependence errors, it limits composition and control over inference, and does not guarantee absence of other types of errors. This paper presents the FLEXI programming model which supports constructs for invoking inference in the language and reusing the results in other statistical computations. We define a novel formalism for inference with a Decorated Bayesian Network and present a tool, DePP, that analyzes this representation to identify the above errors. We evaluate DePP on a range of prototypical examples to show how it helps developers to detect errors. @InProceedings{MAPL17p18, author = {Chandrakana Nandi and Dan Grossman and Adrian Sampson and Todd Mytkowicz and Kathryn S. McKinley}, title = {Debugging Probabilistic Programs}, booktitle = {Proc.\ MAPL}, publisher = {ACM}, pages = {1826}, doi = {10.1145/3088525.3088564}, year = {2017}, } Publisher's Version Article Search 

Murphy, Charlie 
MAPL '17: "Verified Perceptron Convergence ..."
Verified Perceptron Convergence Theorem
Charlie Murphy, Patrick Gray, and Gordon Stewart (Princeton University, USA; Ohio University, USA) Frank Rosenblatt invented the perceptron algorithm in 1957 as part of an early attempt to build ``brain models'', artificial neural networks. In this paper, we apply tools from symbolic logic such as dependent type theory as implemented in Coq to build, and prove convergence of, onelayer perceptrons (specifically, we show that our Coq implementation converges to a binary classifier when trained on linearly separable datasets). Our perceptron and proof are extensible, which we demonstrate by adapting our convergence proof to the averaged perceptron, a common variant of the basic perceptron algorithm. We perform experiments to evaluate the performance of our Coq perceptron vs. an arbitraryprecision C++ implementation and against a hybrid implementation in which separators learned in C++ are certified in Coq. We find that by carefully optimizing the extraction of our Coq perceptron, we can meet  and occasionally exceed  the performance of the arbitraryprecision C++ implementation. Our hybrid Coq certifier demonstrates an architecture for building highassurance machinelearning systems that reuse existing codebases. @InProceedings{MAPL17p43, author = {Charlie Murphy and Patrick Gray and Gordon Stewart}, title = {Verified Perceptron Convergence Theorem}, booktitle = {Proc.\ MAPL}, publisher = {ACM}, pages = {4350}, doi = {10.1145/3088525.3088673}, year = {2017}, } Publisher's Version Article Search Info 

Murray, Derek G. 
MAPL '17: "A Computational Model for ..."
A Computational Model for TensorFlow: An Introduction
Martín Abadi, Michael Isard, and Derek G. Murray (Google Brain, USA) TensorFlow is a powerful, programmable system for machine learning. This paper aims to provide the basics of a conceptual framework for understanding the behavior of TensorFlow models during training and inference: it describes an operational semantics, of the kind common in the literature on programming languages. More broadly, the paper suggests that a programminglanguage perspective is fruitful in designing and in explaining systems such as TensorFlow. @InProceedings{MAPL17p1, author = {Martín Abadi and Michael Isard and Derek G. Murray}, title = {A Computational Model for TensorFlow: An Introduction}, booktitle = {Proc.\ MAPL}, publisher = {ACM}, pages = {17}, doi = {10.1145/3088525.3088527}, year = {2017}, } Publisher's Version Article Search 

Mytkowicz, Todd 
MAPL '17: "Debugging Probabilistic Programs ..."
Debugging Probabilistic Programs
Chandrakana Nandi, Dan Grossman, Adrian Sampson, Todd Mytkowicz, and Kathryn S. McKinley (University of Washington, USA; Cornell University, USA; Microsoft Research, USA; Google, USA) Many applications compute with estimated and uncertain data. While advances in probabilistic programming help developers build such applications, debugging them remains extremely challenging. New types of errors in probabilistic programs include 1) ignoring dependencies and correlation between random variables and in training data, 2) poorly chosen inference hyperparameters, and 3) incorrect statistical models. A partial solution to prevent these errors in some languages forbids developers from explicitly invoking inference. While this prevents some dependence errors, it limits composition and control over inference, and does not guarantee absence of other types of errors. This paper presents the FLEXI programming model which supports constructs for invoking inference in the language and reusing the results in other statistical computations. We define a novel formalism for inference with a Decorated Bayesian Network and present a tool, DePP, that analyzes this representation to identify the above errors. We evaluate DePP on a range of prototypical examples to show how it helps developers to detect errors. @InProceedings{MAPL17p18, author = {Chandrakana Nandi and Dan Grossman and Adrian Sampson and Todd Mytkowicz and Kathryn S. McKinley}, title = {Debugging Probabilistic Programs}, booktitle = {Proc.\ MAPL}, publisher = {ACM}, pages = {1826}, doi = {10.1145/3088525.3088564}, year = {2017}, } Publisher's Version Article Search 

Naik, Mayur 
MAPL '17: "Combining the Logical and ..."
Combining the Logical and the Probabilistic in Program Analysis
Xin Zhang, Xujie Si, and Mayur Naik (Georgia Institute of Technology, USA; University of Pennsylvania, USA) Conventional program analyses have made great strides by leveraging logical reasoning. However, they cannot handle uncertain knowledge, and they lack the ability to learn and adapt. This in turn hinders the accuracy, scalability, and usability of program analysis tools in practice. We seek to address these limitations by proposing a methodology and framework for incorporating probabilistic reasoning directly into existing program analyses that are based on logical reasoning. We demonstrate that the combined approach can benefit a number of important applications of program analysis and thereby facilitate more widespread adoption of this technology. @InProceedings{MAPL17p27, author = {Xin Zhang and Xujie Si and Mayur Naik}, title = {Combining the Logical and the Probabilistic in Program Analysis}, booktitle = {Proc.\ MAPL}, publisher = {ACM}, pages = {2734}, doi = {10.1145/3088525.3088563}, year = {2017}, } Publisher's Version Article Search 

Nandi, Chandrakana 
MAPL '17: "Debugging Probabilistic Programs ..."
Debugging Probabilistic Programs
Chandrakana Nandi, Dan Grossman, Adrian Sampson, Todd Mytkowicz, and Kathryn S. McKinley (University of Washington, USA; Cornell University, USA; Microsoft Research, USA; Google, USA) Many applications compute with estimated and uncertain data. While advances in probabilistic programming help developers build such applications, debugging them remains extremely challenging. New types of errors in probabilistic programs include 1) ignoring dependencies and correlation between random variables and in training data, 2) poorly chosen inference hyperparameters, and 3) incorrect statistical models. A partial solution to prevent these errors in some languages forbids developers from explicitly invoking inference. While this prevents some dependence errors, it limits composition and control over inference, and does not guarantee absence of other types of errors. This paper presents the FLEXI programming model which supports constructs for invoking inference in the language and reusing the results in other statistical computations. We define a novel formalism for inference with a Decorated Bayesian Network and present a tool, DePP, that analyzes this representation to identify the above errors. We evaluate DePP on a range of prototypical examples to show how it helps developers to detect errors. @InProceedings{MAPL17p18, author = {Chandrakana Nandi and Dan Grossman and Adrian Sampson and Todd Mytkowicz and Kathryn S. McKinley}, title = {Debugging Probabilistic Programs}, booktitle = {Proc.\ MAPL}, publisher = {ACM}, pages = {1826}, doi = {10.1145/3088525.3088564}, year = {2017}, } Publisher's Version Article Search 

Porter, Adam A. 
MAPL '17: "Learning a Classifier for ..."
Learning a Classifier for False Positive Error Reports Emitted by Static Code Analysis Tools
Ugur Koc, Parsa Saadatpanah, Jeffrey S. Foster, and Adam A. Porter (University of Maryland at College Park, USA) The large scale and high complexity of modern software systems make perfectly precise static code analysis (SCA) infeasible. Therefore SCA tools often overapproximate, so not to miss any real problems. This, however, comes at the expense of raising false alarms, which, in practice, reduces the usability of these tools. To partially address this problem, we propose a novel learning process whose goal is to discover program structures that cause a given SCA tool to emit false error reports, and then to use this information to predict whether a new error report is likely to be a false positive as well. To do this, we first preprocess code to isolate the locations that are related to the error report. Then, we apply machine learning techniques to the preprocessed code to discover correlations and to learn a classifier. We evaluated this approach in an initial case study of a widelyused SCA tool for Java. Our results showed that for our dataset we could accurately classify a large majority of false positive error reports. Moreover, we identified some common coding patterns that led to false positive errors. We believe that SCA developers may be able to redesign their methods to address these patterns and reduce false positive error reports. @InProceedings{MAPL17p35, author = {Ugur Koc and Parsa Saadatpanah and Jeffrey S. Foster and Adam A. Porter}, title = {Learning a Classifier for False Positive Error Reports Emitted by Static Code Analysis Tools}, booktitle = {Proc.\ MAPL}, publisher = {ACM}, pages = {3542}, doi = {10.1145/3088525.3088675}, year = {2017}, } Publisher's Version Article Search 

Saadatpanah, Parsa 
MAPL '17: "Learning a Classifier for ..."
Learning a Classifier for False Positive Error Reports Emitted by Static Code Analysis Tools
Ugur Koc, Parsa Saadatpanah, Jeffrey S. Foster, and Adam A. Porter (University of Maryland at College Park, USA) The large scale and high complexity of modern software systems make perfectly precise static code analysis (SCA) infeasible. Therefore SCA tools often overapproximate, so not to miss any real problems. This, however, comes at the expense of raising false alarms, which, in practice, reduces the usability of these tools. To partially address this problem, we propose a novel learning process whose goal is to discover program structures that cause a given SCA tool to emit false error reports, and then to use this information to predict whether a new error report is likely to be a false positive as well. To do this, we first preprocess code to isolate the locations that are related to the error report. Then, we apply machine learning techniques to the preprocessed code to discover correlations and to learn a classifier. We evaluated this approach in an initial case study of a widelyused SCA tool for Java. Our results showed that for our dataset we could accurately classify a large majority of false positive error reports. Moreover, we identified some common coding patterns that led to false positive errors. We believe that SCA developers may be able to redesign their methods to address these patterns and reduce false positive error reports. @InProceedings{MAPL17p35, author = {Ugur Koc and Parsa Saadatpanah and Jeffrey S. Foster and Adam A. Porter}, title = {Learning a Classifier for False Positive Error Reports Emitted by Static Code Analysis Tools}, booktitle = {Proc.\ MAPL}, publisher = {ACM}, pages = {3542}, doi = {10.1145/3088525.3088675}, year = {2017}, } Publisher's Version Article Search 

Sampson, Adrian 
MAPL '17: "Debugging Probabilistic Programs ..."
Debugging Probabilistic Programs
Chandrakana Nandi, Dan Grossman, Adrian Sampson, Todd Mytkowicz, and Kathryn S. McKinley (University of Washington, USA; Cornell University, USA; Microsoft Research, USA; Google, USA) Many applications compute with estimated and uncertain data. While advances in probabilistic programming help developers build such applications, debugging them remains extremely challenging. New types of errors in probabilistic programs include 1) ignoring dependencies and correlation between random variables and in training data, 2) poorly chosen inference hyperparameters, and 3) incorrect statistical models. A partial solution to prevent these errors in some languages forbids developers from explicitly invoking inference. While this prevents some dependence errors, it limits composition and control over inference, and does not guarantee absence of other types of errors. This paper presents the FLEXI programming model which supports constructs for invoking inference in the language and reusing the results in other statistical computations. We define a novel formalism for inference with a Decorated Bayesian Network and present a tool, DePP, that analyzes this representation to identify the above errors. We evaluate DePP on a range of prototypical examples to show how it helps developers to detect errors. @InProceedings{MAPL17p18, author = {Chandrakana Nandi and Dan Grossman and Adrian Sampson and Todd Mytkowicz and Kathryn S. McKinley}, title = {Debugging Probabilistic Programs}, booktitle = {Proc.\ MAPL}, publisher = {ACM}, pages = {1826}, doi = {10.1145/3088525.3088564}, year = {2017}, } Publisher's Version Article Search 

Si, Xujie 
MAPL '17: "Combining the Logical and ..."
Combining the Logical and the Probabilistic in Program Analysis
Xin Zhang, Xujie Si, and Mayur Naik (Georgia Institute of Technology, USA; University of Pennsylvania, USA) Conventional program analyses have made great strides by leveraging logical reasoning. However, they cannot handle uncertain knowledge, and they lack the ability to learn and adapt. This in turn hinders the accuracy, scalability, and usability of program analysis tools in practice. We seek to address these limitations by proposing a methodology and framework for incorporating probabilistic reasoning directly into existing program analyses that are based on logical reasoning. We demonstrate that the combined approach can benefit a number of important applications of program analysis and thereby facilitate more widespread adoption of this technology. @InProceedings{MAPL17p27, author = {Xin Zhang and Xujie Si and Mayur Naik}, title = {Combining the Logical and the Probabilistic in Program Analysis}, booktitle = {Proc.\ MAPL}, publisher = {ACM}, pages = {2734}, doi = {10.1145/3088525.3088563}, year = {2017}, } Publisher's Version Article Search 

Stewart, Gordon 
MAPL '17: "Verified Perceptron Convergence ..."
Verified Perceptron Convergence Theorem
Charlie Murphy, Patrick Gray, and Gordon Stewart (Princeton University, USA; Ohio University, USA) Frank Rosenblatt invented the perceptron algorithm in 1957 as part of an early attempt to build ``brain models'', artificial neural networks. In this paper, we apply tools from symbolic logic such as dependent type theory as implemented in Coq to build, and prove convergence of, onelayer perceptrons (specifically, we show that our Coq implementation converges to a binary classifier when trained on linearly separable datasets). Our perceptron and proof are extensible, which we demonstrate by adapting our convergence proof to the averaged perceptron, a common variant of the basic perceptron algorithm. We perform experiments to evaluate the performance of our Coq perceptron vs. an arbitraryprecision C++ implementation and against a hybrid implementation in which separators learned in C++ are certified in Coq. We find that by carefully optimizing the extraction of our Coq perceptron, we can meet  and occasionally exceed  the performance of the arbitraryprecision C++ implementation. Our hybrid Coq certifier demonstrates an architecture for building highassurance machinelearning systems that reuse existing codebases. @InProceedings{MAPL17p43, author = {Charlie Murphy and Patrick Gray and Gordon Stewart}, title = {Verified Perceptron Convergence Theorem}, booktitle = {Proc.\ MAPL}, publisher = {ACM}, pages = {4350}, doi = {10.1145/3088525.3088673}, year = {2017}, } Publisher's Version Article Search Info 

Vieira, Tim 
MAPL '17: "Dyna: Toward a SelfOptimizing ..."
Dyna: Toward a SelfOptimizing Declarative Language for Machine Learning Applications
Tim Vieira, Matthew FrancisLandau, Nathaniel Wesley Filardo, Farzad Khorasani, and Jason Eisner (Johns Hopkins University, USA; Rice University, USA) Declarative programming is a paradigm that allows programmers to specify what they want to compute, leaving how to compute it to a solver. Our declarative programming language, Dyna, is designed to compactly specify computations like those that are frequently encountered in machine learning. As a declarative language, Dyna’s solver has a large space of (correct) strategies available to it. We describe a reinforcement learning framework for adaptively choosing among these strategies to maximize efficiency for a given workload. Adaptivity in execution is especially important for software that will run under a variety of workloads, where no fixed policy works well. We hope that reinforcement learning will identify good policies reasonably quickly—offloading the burden of writing efficient code from human programmers. @InProceedings{MAPL17p8, author = {Tim Vieira and Matthew FrancisLandau and Nathaniel Wesley Filardo and Farzad Khorasani and Jason Eisner}, title = {Dyna: Toward a SelfOptimizing Declarative Language for Machine Learning Applications}, booktitle = {Proc.\ MAPL}, publisher = {ACM}, pages = {817}, doi = {10.1145/3088525.3088562}, year = {2017}, } Publisher's Version Article Search 

Zhang, Xin 
MAPL '17: "Combining the Logical and ..."
Combining the Logical and the Probabilistic in Program Analysis
Xin Zhang, Xujie Si, and Mayur Naik (Georgia Institute of Technology, USA; University of Pennsylvania, USA) Conventional program analyses have made great strides by leveraging logical reasoning. However, they cannot handle uncertain knowledge, and they lack the ability to learn and adapt. This in turn hinders the accuracy, scalability, and usability of program analysis tools in practice. We seek to address these limitations by proposing a methodology and framework for incorporating probabilistic reasoning directly into existing program analyses that are based on logical reasoning. We demonstrate that the combined approach can benefit a number of important applications of program analysis and thereby facilitate more widespread adoption of this technology. @InProceedings{MAPL17p27, author = {Xin Zhang and Xujie Si and Mayur Naik}, title = {Combining the Logical and the Probabilistic in Program Analysis}, booktitle = {Proc.\ MAPL}, publisher = {ACM}, pages = {2734}, doi = {10.1145/3088525.3088563}, year = {2017}, } Publisher's Version Article Search 
23 authors
proc time: 0.87