PPL 2024
論理関係によるshift/reset の部分評価器の正当性の証明
Asai 2006(お茶の水女子大学の浅井先生の論文)の中に誤りがあったので、let-insertionの概念を用いて再度証明した
shift/reset (限定継続)の話
Olivier Danvy and Andrzej Filinski. 1990. Abstracting control. In Proceedings of the 1990 ACM conference on LISP and functional programming (LFP ’90). Association for Computing Machinery, New York, NY, USA, 151–160. https://doi.org/10.1145/91556.91622 （shift/resetの初出）
Q/A 束縛時解析が思ったより微妙だったという話らしい（型の制約的に）
(この手の証明を理解するにはどんな訓練をすればよいのか？)意味論
Compilation Semantics for a Programming Language with Versions
外部パッケージをアップデートするとき、プログラム全体の呼び出しを新しいものに変えないといけないから、いい感じにバージョンを混在させる仕組みがほしい
既存の手法( $ \lambda _{VL}) はプログラムの中にアノテーションをつける
明示的に指定しないアイデア
→モジュールごとにバージョンを指定
Answer Refinement ModificationRefinement Type System for Algebraic Effects and Handlers
篩型
refinement types
1+2 : {x: int | x = 3}
1+2 : {x: int | x > 0}
より詳しい型みたいなかんじ
Answer type modification
Answer type →文脈（外側の継続）の型 （継続が返す型）
let多相 (キーワード)
解集合プログラミング
↑論理プログラミングの話
Regular Expressions with Backreferences on MCFL, and Star-Closedness
REwB(後方参照付きの正規表現)の表現能力（言語クラス？）の話
https://scrapbox.io/files/65e9555c31aa3b00253543c9.png
言語クラスの包含関係をどうやって示すのか証明方法を調べる
rewbはNUR(未定義の参照を持たない)
star-closedness制を使ってMCFLに含まれることを証明するとき、いくつメモリを用意すればいい？の話
https://scrapbox.io/files/65e95814b6479f00257c28f4.png
s17-2-稲葉-新屋-中村-山口
Google RE2
Boyer-Moore法（正規表現のマッチング判定に、正規表現の部分文字列(キーワード)）で高速化する
要は、文字列が言語に含まれるかを判定するために、正規表現が受理する言語Aよりも遥かに大きな（しかし$ \Sigma ^*よりは十分に小さい)言語に含まれるかを検査する
- 文字検査可能
- 一般化有限確定
- 区分検査可能
PSPACE完全（キーワード）
↑星無し(Star Free Language)
C可測性
Repairing Regular Expressions for Extraction
正規表現の利用法
Membership Testing / Extraction
文字列が受理するか / 受理する部分を抽出 or false
Extractionのタスクに対して、自動的に正規表現を修正する候補を提示するものを作成