POPL

\documentclass[acmsmall,screen]{acmart}
\acmJournal{PACMPL}
\acmVolume{8} \acmNumber{POPL} \acmArticle{42}
\acmYear{2026} \acmMonth{1}
\acmDOI{10.1145/XXXXXXX.XXXXXXX}

\usepackage{amsmath,amssymb,amsthm,mathtools}
\usepackage{mathpartir}
\usepackage{booktabs}

\newtheorem{theorem}{Theorem}
\newtheorem{lemma}[theorem]{Lemma}
\theoremstyle{definition}
\newtheorem{definition}[theorem]{Definition}

\begin{document}

\title{A Sound and Complete Type System for\\
       Probabilistic Programs with Higher-Order Features}

\author{First Last}
\affiliation{\institution{University of Example}\country{Country}}
\email{[email protected]}
\author{Jane Doe}
\affiliation{\institution{Example Research Labs}\country{Country}}
\email{[email protected]}
\renewcommand{\shortauthors}{Last and Doe}

\begin{abstract}
We give the first sound and complete type system for a probabilistic
programming language with higher-order functions and continuous
distributions. Our system uses modal types to track measurability of
terms and ensures that all well-typed programs denote a well-defined
measure kernel.
\end{abstract}

\begin{CCSXML}
<ccs2012><concept><concept_id>10011007.10011006</concept_id>
<concept_desc>Software and its engineering~Functional languages</concept_desc></concept></ccs2012>
\end{CCSXML}
\ccsdesc[500]{Software and its engineering~Functional languages}
\keywords{probabilistic programming, type systems, measure theory}
\maketitle

\section{Introduction}
Probabilistic programming languages are increasingly used, but their
semantic foundations remain fragile when higher-order features meet
continuous distributions.

\section{Preliminaries}
Let $\lambda_\mathrm{PP}$ denote our core language with lambda
abstraction, application, sample, and conditioning.

\section{Type System}
\begin{mathpar}
  \inferrule{\Gamma \vdash e : \tau_1 \to \tau_2 \\ \Gamma \vdash e' : \tau_1}
            {\Gamma \vdash e\, e' : \tau_2}
  \and
  \inferrule{\Gamma \vdash e : \textsf{Meas}\, \tau}
            {\Gamma \vdash \mathsf{sample}\, e : \tau}
\end{mathpar}

\begin{definition}[Measurability]
A type is \emph{measurable} if its values inhabit a standard Borel space.
\end{definition}

\section{Soundness}
\begin{theorem}[Soundness]
If $\vdash e : \tau$ then $\llbracket e \rrbracket$ denotes a well-defined
measure kernel of type $\tau$.
\end{theorem}
\begin{proof}
By induction on the typing derivation.
\end{proof}

\section{Completeness and Decidability}
\begin{theorem}[Completeness]
Every program denoting a well-defined measure kernel is well-typed.
\end{theorem}

Type-checking reduces to deciding measurability of arithmetic terms,
which we outsource to an SMT-based oracle.

\section{Implementation}
We implemented a type checker in 4{,}200 LOC of OCaml and evaluated it
on 80 benchmark programs.

\section{Conclusion}
A principled type system bridges higher-order probabilistic programs
and measure-theoretic semantics.

\bibliographystyle{ACM-Reference-Format}
\bibliography{refs}
\end{document}