論文の概要: Kotlin's Type System is (Also) Unsound

• arxiv url: http://arxiv.org/abs/2408.10804v1
• Date: Tue, 20 Aug 2024 12:54:12 GMT
• ステータス: 処理完了
• システム内更新日: 2024-08-21 13:45:16.780416
• Title: Kotlin's Type System is (Also) Unsound
• Title（参考訳）: Kotlinの型システムは(Also)正しくない
• Authors: Elad Kinsbruner, Hila Peleg, Shachar Itzhaky,
• Abstract要約: 音型システムの型チェッカーは、型エラー毎に警告を発することが期待されている。 2016年、Amin氏とTate氏は、JavaとScalaという2つの主要な産業言語に対して、最初の不健全な証明を提示した。 我々は、これまで未知の言語機能の組み合わせに依存していたKotlinの不健全性証明を提示する。
• 参考スコア（独自算出の注目度）: 0.19116784879310028
• License: http://creativecommons.org/licenses/by-sa/4.0/
• Abstract: Soundness of a type system is a fundemental property that guarantees that no operation that is not supported by a value will be performed on that value at run time. A type checker for a sound type system is expected to issue a warning on every type error. While soundness is a desirable property for many practical applications, in 2016, Amin and Tate presented the first unsoundness proof for two major industry languages: Java and Scala. This proof relied on use-site variance and implicit null values. We present an unsoundness proof for Kotlin, another emerging industry language, which relies on a previously unknown unsound combination of language features. Kotlin does not have implicit null values, meaning that the proof by Amin and Tate would not work for Kotlin. Our new proof, which is an infringing code snippet, utilizes Kotlin's \emph{declaration-site} variance specification and does not require implicit null values. We present this counterexample to soundness in full along with detailed explanations of every step. Finally, we present a thorough discussion on precisely which language features cause this issue, as well as how Kotlin's compiler can be patched to fix it.
• Abstract（参考訳）: 型システムの健全性(英: Soundness of a type system)は、実行時にその値に対して、値によってサポートされない操作が実行されないことを保証する、資金的特性である。 音型システムの型チェッカーは、型エラー毎に警告を発することが期待されている。 健全性は多くの実用的なアプリケーションにとって望ましい特性であるが、2016年、Amin氏とTate氏はJavaとScalaの2つの主要な産業言語に対する最初の不健全性証明を提示した。 この証明は、使用部位の分散と暗黙のnull値に依存していた。 私たちは、これまで未知の言語機能の組み合わせに依存していた、別の新興産業言語であるKotlinに対して、不健全な証明を提示します。 Kotlinには暗黙的なnull値がないため、AminとTateによる証明はKotlinでは機能しない。 我々の新しい証明は、侵害的なコードスニペットであり、Kotlinの \emph{declaration-site} 分散仕様を利用しており、暗黙のnull値を必要としない。 各ステップの詳細な説明とともに、この反例を完全な音性に提示する。 最後に、この問題の原因となる言語機能と、Kotlinのコンパイラにパッチを当てて修正する方法について、徹底的な議論を行う。

関連論文リスト

• Generating Diverse Negations from Affirmative Sentences [0.999726509256195]
  否定は、動詞句、節、その他の表現において負の極性を符号化する現実世界の応用において重要である。 多様な否定型を生成することにより,否定データセットの欠如に対処する手法であるNegVerseを提案する。 我々は,構文構造に基づいて,否定が最も起こりやすい文の一部をマスキングするための新しい規則を提案する。 また, 否定の手がかりを同定し, 退化例を除去し, 多様な有意義な摂動を生じさせるフィルタリング機構を提案する。
  論文  参考訳（メタデータ） (2024-10-30T21:25:02Z)
• How Do Developers Use Type Inference: An Exploratory Study in Kotlin [3.382017614888546]
  KotlinはAndroid開発のデフォルト言語であり、最大のソフトウェアマーケットプレースのひとつです。 ソフトウェアリポジトリをマイニングするツールであるBoaを用いて,大規模な実証的研究を行う。 この結果,ローカル変数や変数に対して,ファイル外でメソッド呼び出しが宣言される場合,型推論が頻繁に使用されることがわかった。
  論文  参考訳（メタデータ） (2024-10-30T18:07:21Z)
• Cross-Language Dependencies: An Empirical Study of Kotlin-Java [1.5680371708311132]
  Googleが2017年にAndroidアプリ開発の公式プログラミング言語としてKotlinを導入して以来、KotlinはAndroid開発で広く採用されている。 現実世界のプロジェクトでJavaとKotlinが相互に相互作用する方法については、限定的な研究がある。 我々は、3,227のJavaと8,630のKotlinソースファイルを持つ23のKotlin-Java実世界のプロジェクトについて実証的研究を行った。
  論文  参考訳（メタデータ） (2024-05-07T18:26:24Z)
• Depends-Kotlin: A Cross-Language Kotlin Dependency Extractor [3.0915964434574175]
  Depends-KotlinはKotlinコード内のエンティティの依存関係の抽出をサポートする。 KotlinとJava間の依存関係関係も抽出できる。 Depends-Kotlinは、Kotlin-KotlinとKotlin-Javaの依存関係関係を解決する際に、高い精度とパフォーマンスを示す。
  論文  参考訳（メタデータ） (2024-01-30T10:15:35Z)
• PTE: Axiomatic Semantics based Compiler Testing [7.203331838793759]
  本稿では,PTEと呼ばれるコンパイラテストのための公理的セマンティクスに基づくアプローチを提案する。 その考え方は、emph(textbfprecondition, textbftransformation, textbfexpectation)という形で言語意味論の逸話を捉えた公理の集合を段階的に発展させることである。
  論文  参考訳（メタデータ） (2024-01-02T04:50:47Z)
• Generative Type Inference for Python [62.01560866916557]
  本稿では静的解析から静的ドメイン知識を取り入れた数ショットの生成型推論手法であるTypeGenを紹介する。 TypeGenは、静的解析の型推論ステップを、型依存グラフ(TDG)に基づいたプロンプトに変換することで、COTプロンプトを生成する。 実験の結果、TypeGenは引数型予測では10.0%、Top-1 Exact Matchでは22.5%で最高のベースラインであるType4Pyを上回っている。
  論文  参考訳（メタデータ） (2023-07-18T11:40:31Z)
• Efficient Semiring-Weighted Earley Parsing [71.77514972816347]
  本稿では,様々なスピードアップを伴うEarey (1970) の文脈自由構文解析アルゴリズムの,推論システムという形での参照記述を提供する。 私たちのプレゼンテーションには、Earey氏の$O(N3|GR|)$から、既知の最悪のランタイム改善が含まれています。 半重み付き推論への一般化を扱い、Stolcke (1995)のような文法を前処理して推論サイクルを排除し、さらに文プレフィックスの重みを計算するStolckeの手法を一般化する。
  論文  参考訳（メタデータ） (2023-07-06T13:33:59Z)
• Lexinvariant Language Models [84.2829117441298]
  離散語彙記号から連続ベクトルへの写像であるトークン埋め込みは、任意の言語モデル(LM)の中心にある 我々は、語彙記号に不変であり、したがって実際に固定トークン埋め込みを必要としないテクスチトレキシン変種モデルについて研究する。 十分長い文脈を条件として,レキシン変項LMは標準言語モデルに匹敵する難易度が得られることを示す。
  論文  参考訳（メタデータ） (2023-05-24T19:10:46Z)
• TypeT5: Seq2seq Type Inference using Static Analysis [51.153089609654174]
  本稿では,型予測をコード入力タスクとして扱う新しい型推論手法を提案する。 本手法では静的解析を用いて,型シグネチャがモデルによって予測されるコード要素毎に動的コンテキストを構築する。 また,モデルの入力コンテキストに事前の型予測を組み込んだ反復復号方式を提案する。
  論文  参考訳（メタデータ） (2023-03-16T23:48:00Z)
• Multi-VALUE: A Framework for Cross-Dialectal English NLP [49.55176102659081]
  マルチディレクト (Multi-Dilect) は、50の英語方言にまたがる制御可能なルールベースの翻訳システムである。 ストレステストは、非標準方言の先行モデルに対する顕著な性能格差を示す。 私たちはチカノやインド英語のネイティブスピーカーと提携して、人気のあるCoQAタスクの新しいゴールドスタンダード版をリリースしています。
  論文  参考訳（メタデータ） (2022-12-15T18:17:01Z)
• Not another Negation Benchmark: The NaN-NLI Test Suite for Sub-clausal Negation [59.307534363825816]
  否定は現在の言語モデルでは不十分だが、この問題の範囲は広く理解されていない。 自然言語推論(NLI)テストスイートを導入し,NLP手法の能力を検証した。
  論文  参考訳（メタデータ） (2022-10-06T23:39:01Z)

関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。

指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。