ベビーモジュラ3
Baby Modula-3は、 Martín Abadiによって考案された理念に基づく、Modula-3(セーフサブセット)プログラミング言語の関数型プログラミングサブ言語です。プログラミング言語設計の研究を目的としたオブジェクト指向プログラミング言語であり、一部は暗黙的にプロトタイプ指向であり、他の部分は明示的に静的型付けされており、コンピュータサイエンスの型理論の研究を目的としています。メタプログラミングシステムの形式言語として検証されています。[ 1 ]スカンジナビアのオブジェクト指向言語 学派に由来します。
アバディは、オブジェクトの形式意味論を研究できる純粋なオブジェクト指向言語の例を挙げようとした。「Baby Modula-3は、構造化された操作的意味論と一連の静的型規則によって定義されています。表示的意味論によって、この定義の妥当性が保証されています。」[ 1 ] このオブジェクトモデルは、十分な決定可能性(well-definedness decidability)を持つことが示されている[ 2 ](その機械的な証明は知られていない)。
アバディは、カリフォルニア州パロアルトにあるディジタル・イクイップメント・コーポレーション(DEC)のシステム・リサーチ・センター(SRC)に勤務していました。DECがコンパックに買収され、その後コンパックがヒューレット・パッカード(HP)に買収されたため、SRCレポート95はHPによって公開されました。
影響
ルカ・カルデッリとマルティン・アバディは1996年に『オブジェクトの理論』[ 3 ]を著し、オブジェクト指向プログラミング言語の意味論のための形式的計算を提示した。カルデッリによれば、Baby Modula-3はこの研究に影響を与え、[ 4 ] 「オブジェクトの型」におけるselfの型と「self」の型の計算を導いた。[ 5 ]これは、 AdaやCなどの言語の形式的意味論をモデル化するために使用されてきたオブジェクト指向型システムプログラミング言語 のためのModula-3形式的意味論検証システムの研究への道を開いた。[ 6 ]
参考文献
- ^ a b Baby Modula-3と物体理論Archived 2021-05-13 at the Wayback Machine Martin Abadi. Digital Equipment Corporation (DEC) Systems Research Center (SRC) Research Report 95 (February 1993)
- ^ Schwinghammer, J. (2008-01-01). 「オブジェクト計算における評価による正規化について」. Miculan, Marino; Scagnetto, Ivan; Honsell, Furio (編). Types for Proofs and Programs . Lecture Notes in Computer Science. Vol. 4941. Springer Berlin Heidelberg. pp. 173– 187. CiteSeerX 10.1.1.140.5764 . doi : 10.1007/978-3-540-68103-8_12 . ISBN 978-3-540-68084-0。
- ^アバディ, マーティン;カルデッリ, ルカ(1996-08-09). 『オブジェクトの理論』(訂正版). シュプリンガー. ISBN 978-0387947754。
- ^プリミティブオブジェクトの理論(型なし、第一および第二階層システム)(PDF) 、 2025年9月25日取得
- ^アメリカ数学会論文要旨. アメリカ数学会. 1995年.
- ^研究、 2012年3月22日閲覧