On algebraic structure of functional programming languages: towards mathematical foundation of logical relations
| Project/Area Number |
26730004
|
|---|
| Research Category |
Grant-in-Aid for Young Scientists (B)
|
| Allocation Type | Multi-year Fund |
|---|
| Research Field |
Theory of informatics
|
|---|
| Research Institution | Kyoto University |
|---|
Principal Investigator |
|
|---|
| Project Period (FY) |
2014-04-01 – 2019-03-31
|
| Project Status |
Completed (Fiscal Year 2018)
|
| Budget Amount *help |
¥3,770,000 (Direct Cost: ¥2,900,000、Indirect Cost: ¥870,000)
Fiscal Year 2017: ¥910,000 (Direct Cost: ¥700,000、Indirect Cost: ¥210,000)
Fiscal Year 2016: ¥910,000 (Direct Cost: ¥700,000、Indirect Cost: ¥210,000)
Fiscal Year 2015: ¥910,000 (Direct Cost: ¥700,000、Indirect Cost: ¥210,000)
Fiscal Year 2014: ¥1,040,000 (Direct Cost: ¥800,000、Indirect Cost: ¥240,000)
|
|---|
| Keywords | 論理関係 / 圏論的意味論 / 関数型プログラミング言語 |
|---|
| Outline of Final Research Achievements |
Logical relation is a powerful mathematical technique to prove mathematical properties of functional programming languages such as: observational equivalence of programs, strong normalization of lambda terms and parametricity principle of second-order lambda calculi. The main contribution of this research project is a construction of categorical models for higher-order (high-level) functional programming languages starting from categorical models of first-order (low-level) programming languages. We applied this construction technique to give adequate categorical models for higher-order functional programming languages with algebraic effects and a higher-order functional programming language with continuous probabilistic distribution and "scoring" mechanism. Our construction can be regarded as a program translation technique of higher-order (high-level) programming languages into first-order (low-level) programming languages.
|
| Academic Significance and Societal Importance of the Research Achievements |
本研究の成果からは種々の特徴（代数的副作用や連続的確率分布を扱えるなど）を持った高階の関数型プログラミング言語を同様の特徴を持つ一階のプログラミング言語に変換する手法が得られる．ここでの変換の数学的正しさは変換の導出に用いた論理関係により保証されている．この変換手法を経由することで一階のプログラミング言語の検証手法を高階の関数型プログラミング言語の検証手法に拡張することができると期待される．特に連続的確率分布を扱うプログラミング言語の検証は機械学習の研究の進展によりその重要性が増している．
|
Report
(6 results)
Research Products
(6 results)
