Stable Relations and Abstract Interpretation of Higher-Order Programs

被引：5
作者：
Montagu, Benoit [1 ]
Jensen, Thomas [1 ]
机构：
[1] INRIA, Campus Univ Beaulieu,Ave Gen Leclerc, F-35042 Rennes, France
来源：
PROCEEDINGS OF THE ACM ON PROGRAMMING LANGUAGES-PACMPL | 2020年 / 4卷 / ICFP期
关键词：
static analysis; lambda-calculus; abstract interpretation; correlations; SYSTEM;
D O I：
10.1145/3409001
中图分类号：
TP31 [计算机软件];
学科分类号：
081202 ; 0835 ;
摘要：
We present a novel denotational semantics for the untyped call-by-value lambda-calculus, where terms are interpreted as stable relations, i.e. as binary relations between substitutions and values, enjoying a monotonicity property. The denotation captures the input-output behaviour of higher-order programs, and is proved sound and complete with respect to the operational semantics. The definition also admits a presentation as a program logic. Following the principles of abstract interpretation, we use our denotational semantics as a collecting semantics to derive a modular relational analysis for higher-order programs. The analysis infers equalities between the arguments of a program and its result-a form of frame condition for functional programs.
引用
收藏
页数：30
相关论文
共 53 条
[1]   DOMAIN THEORY IN LOGICAL FORM [J].
ABRAMSKY, S .
ANNALS OF PURE AND APPLIED LOGIC, 1991, 51 (1-2) :1-77
[2]   Inferring Frame Conditions with Static Correlation Analysis [J].
Andreescu, Oana F. ;
Jensen, Thomas ;
Lescuyer, Stephane ;
Montagu, Benoit .
PROCEEDINGS OF THE ACM ON PROGRAMMING LANGUAGES-PACMPL, 2019, 3
[3]   Engineering Formal Metatheory [J].
Aydemir, Brian ;
Chargueraud, Arthur ;
Pierce, Benjamin C. ;
Pollack, Randy ;
Weirich, Stephanie .
POPL'08: PROCEEDINGS OF THE 35TH ANNUAL ACM SIGPLAN-SIGACT SYMPOSIUM ON PRINCIPLES OF PROGRAMMING LANGUAGES, 2008, :3-15
[4]  
Banerjee A., 2003, Mathematical Structures in Computer Science, V13, P87, DOI 10.1017/S0960129502003845
[5]  
Barnett M, 2006, LECT NOTES COMPUT SC, V4111, P364
[6]  
Barnett Mike, 2005, LNCS, V3362, p49S69, DOI [10.1007/978-3, DOI 10.1007/978-3]
[7]  
Bird Richard., 1996, ALGEBRA PROGRAMMING, DOI [10.1007/978-3-642-61455-2_12, DOI 10.1007/978-3-642-61455-2_12]
[8]  
Cachera David., 2010, INTERACTIVE THEOREM, p9S24, DOI [10.1007/978-3-642-14052-5_3, DOI 10.1007/978-3-642-14052-5_3]
[9]   The Locally Nameless Representation [J].
Chargueraud, Arthur .
JOURNAL OF AUTOMATED REASONING, 2012, 49 (03) :363-408
[10]  
Chargueraud Arthur., 2010, PROCEEDING 15 ACM SI, P321, DOI DOI 10.1145/1863543.1863590
123456