パウル・ブラ・レヴィ（Paul Blain Levy）による計算モデルにCall-By-Push-Value（CBPVと略記）があります。最近知ったのですが、昔（20世紀）から有名らしいです。CBPVの理論には、ラムダ計算の拡張である項言語（term language）が登場するのですが、コレ…