Lisp
S式などの利用で有名
リスト構造の再帰的呼び出しによる手続き論的証明パラダイムの代表としても知られる