@article{vytiniotis_differentiable_2019,
title = {The {Differentiable} {Curry}},
url = {https://openreview.net/forum?id=ryxuz9SzDB},
abstract = {We revisit the automatic differentiation (AD) of programs that contain higher-order functions, in a statically typed setting. Our presentation builds on a recent formulation of AD based on...},
urldate = {2019-11-22},
author = {Vytiniotis, Dimitrios and Belov, Dan and Wei, Richard and Plotkin, Gordon and Abadi, Martin},
month = sep,
year = {2019},
note = {ZSCC: 0000000},
keywords = {Automatic differentiation, Differentiation, Programming language theory}
}
@article{law_functional_2019,
title = {Functional probabilistic programming for scalable {Bayesian} modelling},
url = {http://arxiv.org/abs/1908.02062},
abstract = {Bayesian inference involves the specification of a statistical model by a statistician or practitioner, with careful thought about what each parameter represents. This results in particularly interpretable models which can be used to explain relationships present in the observed data. Bayesian models are useful when an experiment has only a small number of observations and in applications where transparency of data driven decisions is important. Traditionally, parameter inference in Bayesian statistics has involved constructing bespoke MCMC (Markov chain Monte Carlo) schemes for each newly proposed statistical model. This results in plausible models not being considered since efficient inference schemes are challenging to develop or implement. Probabilistic programming aims to reduce the barrier to performing Bayesian inference by developing a domain specific language (DSL) for model specification which is decoupled from the parameter inference algorithms. This paper introduces functional programming principles which can be used to develop an embedded probabilistic programming language. Model inference can be carried out using any generic inference algorithm. In this paper Hamiltonian Monte Carlo (HMC) is used, an efficient MCMC method requiring the gradient of the un-normalised log-posterior, calculated using automatic differentiation. The concepts are illustrated using the Scala programming language.},
urldate = {2019-11-27},
journal = {arXiv:1908.02062 [stat]},
author = {Law, Jonathan and Wilkinson, Darren},
month = aug,
year = {2019},
note = {ZSCC: 0000000
arXiv: 1908.02062},
keywords = {Automatic differentiation, Bayesian inference, Differentiation, Implementation, Probabilistic programming, Programming language theory}
}
@article{ehrhard_differentials_2019,
title = {Differentials and distances in probabilistic coherence spaces},
url = {http://arxiv.org/abs/1902.04836},
abstract = {In probabilistic coherence spaces, a denotational model of probabilistic functional languages, mor-phisms are analytic and therefore smooth. We explore two related applications of the corresponding derivatives. First we show how derivatives allow to compute the expectation of execution time in the weak head reduction of probabilistic PCF (pPCF). Next we apply a general notion of "local" differential of morphisms to the proof of a Lipschitz property of these morphisms allowing in turn to relate the observational distance on pPCF terms to a distance the model is naturally equipped with. This suggests that extending probabilistic programming languages with derivatives, in the spirit of the differential lambda-calculus, could be quite meaningful.},
urldate = {2019-11-28},
journal = {arXiv:1902.04836 [cs]},
author = {Ehrhard, Thomas},
month = feb,
year = {2019},
note = {ZSCC: 0000000
arXiv: 1902.04836},
keywords = {Coherence spaces, Denotational semantics, Differential Linear Logic, Differentiation, Linear logic, Probabilistic programming, Programming language theory}
}
@inproceedings{kerjean_higher-order_2019,
address = {Cham},
series = {Lecture {Notes} in {Computer} {Science}},
title = {Higher-{Order} {Distributions} for {Differential} {Linear} {Logic}},
isbn = {978-3-030-17127-8},
doi = {10/ggdmrj},
abstract = {Linear Logic was introduced as the computational counterpart of the algebraic notion of linearity. Differential Linear Logic refines Linear Logic with a proof-theoretical interpretation of the geometrical process of differentiation. In this article, we construct a polarized model of Differential Linear Logic satisfying computational constraints such as an interpretation for higher-order functions, as well as constraints inherited from physics such as a continuous interpretation for spaces. This extends what was done previously by Kerjean for first order Differential Linear Logic without promotion. Concretely, we follow the previous idea of interpreting the exponential of Differential Linear Logic as a space of higher-order distributions with compact-support, which is constructed as an inductive limit of spaces of distributions on Euclidean spaces. We prove that this exponential is endowed with a co-monadic like structure, with the notable exception that it is functorial only on isomorphisms. Interestingly, as previously argued by Ehrhard, this still allows the interpretation of differential linear logic without promotion.},
language = {en},
booktitle = {Foundations of {Software} {Science} and {Computation} {Structures}},
publisher = {Springer International Publishing},
author = {Kerjean, Marie and Pacaud Lemay, Jean-Simon},
editor = {Bojańczyk, Mikołaj and Simpson, Alex},
year = {2019},
note = {ZSCC: NoCitationData[s1]},
keywords = {Denotational semantics, Differential Linear Logic, Differentiation, Linear logic},
pages = {330--347}
}
@misc{kammar_diffeological_2018,
title = {Diffeological {Spaces} and {Denotational} {Semantics} for {Differential} {Programming}},
language = {en},
author = {Kammar, Ohad and Staton, Sam and Vákár, Matthijs},
year = {2018},
note = {ZSCC: NoCitationData[s1]},
keywords = {Automatic differentiation, Differentiation, Programming language theory}
}
@article{ehrhard_introduction_2016,
title = {An introduction to {Differential} {Linear} {Logic}: proof-nets, models and antiderivatives},
shorttitle = {An introduction to {Differential} {Linear} {Logic}},
url = {http://arxiv.org/abs/1606.01642},
abstract = {Differential Linear Logic enriches Linear Logic with additional logical rules for the exponential connectives, dual to the usual rules of dereliction, weakening and contraction. We present a proof-net syntax for Differential Linear Logic and a categorical axiomatization of its denotational models. We also introduce a simple categorical condition on these models under which a general antiderivative operation becomes available. Last we briefly describe the model of sets and relations and give a more detailed account of the model of finiteness spaces and linear and continuous functions.},
urldate = {2019-11-28},
journal = {arXiv:1606.01642 [cs]},
author = {Ehrhard, Thomas},
month = jun,
year = {2016},
note = {ZSCC: 0000002
arXiv: 1606.01642},
keywords = {Denotational semantics, Differential Linear Logic, Differentiation, Linear logic}
}
@article{manzyuk_simply_2012,
series = {Proceedings of the 28th {Conference} on the {Mathematical} {Foundations} of {Programming} {Semantics} ({MFPS} {XXVIII})},
title = {A {Simply} {Typed} λ-{Calculus} of {Forward} {Automatic} {Differentiation}},
volume = {286},
issn = {1571-0661},
url = {http://www.sciencedirect.com/science/article/pii/S1571066112000473},
doi = {10/ggdm57},
abstract = {We present an extension of the simply typed λ-calculus with pushforward operators. This extension is motivated by the desire to incorporate forward automatic differentiation, which is an important technique in numeric computing, into functional programming. Our calculus is similar to Ehrhard and Regnierʼs differential λ-calculus, but is based on the differential geometric idea of pushforward rather than derivative. We prove that, like the differential λ-calculus, our calculus can be soundly interpreted in differential λ-categories.},
language = {en},
urldate = {2019-11-28},
journal = {Electronic Notes in Theoretical Computer Science},
author = {Manzyuk, Oleksandr},
month = sep,
year = {2012},
note = {ZSCC: 0000013},
keywords = {Automatic differentiation, Differentiation, Programming language theory},
pages = {257--272}
}
@article{fiore_cartesian_2008,
title = {The cartesian closed bicategory of generalised species of structures},
volume = {77},
issn = {00246107},
url = {http://doi.wiley.com/10.1112/jlms/jdm096},
doi = {10/bd2mr9},
abstract = {The concept of generalised species of structures between small categories and, correspondingly, that of generalised analytic functor between presheaf categories are introduced. An operation of substitution for generalised species, which is the counterpart to the composition of generalised analytic functors, is also put forward. These deﬁnitions encompass most notions of combinatorial species considered in the literature—including of course Joyal’s original notion—together with their associated substitution operation. Our ﬁrst main result exhibits the substitution calculus of generalised species as arising from a Kleisli bicategory for a pseudo-comonad on profunctors. Our second main result establishes that the bicategory of generalised species of structures is cartesian closed.},
language = {en},
number = {1},
urldate = {2019-11-28},
journal = {Journal of the London Mathematical Society},
author = {Fiore, M. and Gambino, N. and Hyland, M. and Winskel, G.},
month = feb,
year = {2008},
note = {ZSCC: 0000067},
keywords = {Denotational semantics, Differential Linear Logic, Differentiation, Linear logic},
pages = {203--220}
}
@article{ehrhard_differential_2003,
title = {The differential lambda-calculus},
volume = {309},
issn = {0304-3975},
url = {http://www.sciencedirect.com/science/article/pii/S030439750300392X},
doi = {10/bf3b8v},
abstract = {We present an extension of the lambda-calculus with differential constructions. We state and prove some basic results (confluence, strong normalization in the typed case), and also a theorem relating the usual Taylor series of analysis to the linear head reduction of lambda-calculus.},
language = {en},
number = {1},
urldate = {2019-11-24},
journal = {Theoretical Computer Science},
author = {Ehrhard, Thomas and Regnier, Laurent},
month = dec,
year = {2003},
note = {ZSCC: 0000307},
keywords = {Differentiation, Linear logic, Programming language theory},
pages = {1--41}
}