抄録/ポイント：
抄録/ポイント
文献の概要を数百字程度の日本語でまとめたものです。
部分表示の続きは、JDreamⅢ(有料)でご覧頂けます。
J-GLOBALでは書誌(タイトル、著者名等)登載から半年以上経過後に表示されますが、医療系文献の場合はMyJ-GLOBALでのログインが必要です。
段階的タイピングに関する研究は,SiekとTaha(2006)のGradely Typed Lambda Calculus(GTLC)と,その基礎となる鋳造計算に多くの変化をもたらした。例えば,WadlerとFindler(2009)追加blame追跡,Siek et al.(2009)は,代替鋳造評価戦略を研究し,Hermanら(2010)は,空間効率のためのコーセーションでキャストした。また,GTLCのメタ理論は,blame安全性(Tobin-HochstadtとFeleisen2006),空間消費(Herman et al.2010),および段階的保証(Siek et al.2015)を含むタイプ安全性を超えて拡大した。これらの結果は,GTLCのいくつかの変化に対して証明されたが,他のものではなかった。さらに,研究者はGTLCに関する変化を開発し続けているが,新しい変動に対する全てのメタ理論を確立することは時間がかかる。本論文は,2つのパラメータ化鋳造計算の形式で,多くの鋳造結石間の類似性を捉える抽象を同定し,1つは言語仕様の目的であり,もう1つは空間効率の良い実装をガイドする。本論文は,次に,これらの2つの結石のための再利用可能メタ理論を開発し,タイプ安全性,ブレーム安全性,段階的保証,および空間消費を証明した。最後に,文献から5つと3つの新結石を含む8つの鋳造結石に対するこのメタ理論を具体化した。これらの定義と定理のすべては,2つのパラメータ化計算,再利用可能なメタ理論,および8つのインスタントレーションを含み,モジュールパラメータおよび依存記録の広範囲な利用を,抽象化を定義するために,Agdaで機械化した。【JST・京大機械翻訳】
