Abstract
Stan is a probabilistic programming language that has been increasingly usedfor real-world scalable projects. However, to make practical inferencepossible, the language sacrifices some of its usability by adopting a blocksyntax, which lacks compositionality and flexible user-defined functions.Moreover, the semantics of the language has been mainly given in terms ofintuition about implementation, and has not been formalised. This paper provides a formal treatment of the Stan language, and introducesthe probabilistic programming language SlicStan --- a compositional,self-optimising version of Stan. Our main contributions are: (1) theformalisation of a core subset of Stan through an operational density-basedsemantics; (2) the design and semantics of the Stan-like language SlicStan,which facilities better code reuse and abstraction through its compositionalsyntax, more flexible functions, and information-flow type system; and (3) aformal, semantic-preserving procedure for translating SlicStan to Stan.