Posts

This post aims at reproducing some results from Saad et al.’s paper on Bayesian synthesis1 in OCaml, an industrial strength functional programming language. A complete notebook for the code in this post can be found here.

人们近年来在人工智能领域取得的进展，除了层出不穷的新算法，也

本文参考了 Zachary Kincaid 和 Thomas Reps 在 CAV 2021 上的关于代数程序分析（Algebr

简单地说，程序的资源分析（Resource Analysis）

Tool link: Emacs Syntax Highlighting for LaTeX (ESH). The tool does not really require understanding Emacs: one just needs a working installation! The tool seems well tested on GNU/Linux; however, I am mainly using macOS, so I find out an easy workflow that works for me.

In this post, we consider one-dimensional random walks: assume that $S_n = \sum_{i=1}^n X_i$ is a random walk on the integers with initial value $S_0 = 0$, where $X_i, i \in \mathbb{N}$ are independent and identically distributed random variables.

Problem link: Counting Road Networks | HackerRank. You are supposed to count the number of connected undirected labeled graphs with $n$ vertices. Algorithms with $O(n \log^2 n)$ time complexity are preferable.

Suppose you have a toy specification with built-in nondeterminism, and you want to generate answers with respect to the specification: type exp = EInt of int | EPair of exp * exp | ENdet of exp * exp type ans = VInt of int | VPair of ans * ans For example, from the following specification