Research projects spring 2016
0 likes443 views
Research projects for students of Academic University and Computer Science Center . Saint-Petersburg, 2016.
![弌亠亳亳从舒亳仂仆仆仂亠 仗仂亞舒仄仄亳仂于舒仆亳亠
F* (https://www.fstar-lang.org/tutorial/)
Coq
Agda
...
val sort: l:list int ->
Tot (m:list int{sorted m
/ (forall i. mem i l = mem i m)})
(decreases (length l))
let rec sort l = match l with
| [] -> []
| pivot::tl ->
let hi, lo = partition (cmp pivot) tl in
let l = append (sort lo) (pivot::sort hi) in
dedup l
弌亠仄仆 亳亞仂亠于 8 亠于舒仍 2016亞. 9 / 13](https://image.slidesharecdn.com/grigorevpresentation-160208212941/85/Research-projects-spring-2016-9-320.jpg)
Research projects spring 2016
- 1. YaccConstructor 舒亟舒亳 仆舒 于亠亠仆仆亳亶 亠仄亠 2016 于仂: 弌亠仄仆 亳亞仂亠于 舒弍仂舒仂亳 磶从仂于 亳仆仄亠仆仂于 JetBrains 弌舒仆从-亠亠弍亞从亳亶 亞仂亟舒于亠仆仆亶 仆亳于亠亳亠 舒亠仄舒亳从仂-仄亠舒仆亳亠从亳亶 舒从仍亠 8 亠于舒仍 2016亞. 弌亠仄仆 亳亞仂亠于 8 亠于舒仍 2016亞. 1 / 13
- 2. YaccConstructor 仍亠亟仂于舒仆亳 于 仂弍仍舒亳 仍亠从亳亠从仂亞仂 亳 亳仆舒从亳亠从仂亞仂 舒仆舒仍亳亰舒 从亶 亳仂亟仆亶 从仂亟 https://github.com/YaccConstructor 仆仂于仆仂亶 磶从 舒亰舒弍仂从亳 F# 弌亠仄仆 亳亞仂亠于 8 亠于舒仍 2016亞. 2 / 13
- 3. 丐亠弍仂于舒仆亳 从 亰仆舒仆亳礆 亳 仆舒于从舒仄 仆舒从仂仄于仂 仆从亳仂仆舒仍仆仄 仗仂亞舒仄仄亳仂于舒仆亳亠仄 (F# 亳仍亳 OCaml) 仆舒仆亳 于 仂弍仍舒亳 仍亠从亳亠从仂亞仂 亳 亳仆舒从亳亠从仂亞仂 舒仆舒仍亳亰舒 仆舒仆亳 于 仂弍仍舒亳 亠仆亳从 舒仆仍亳亳 丕仄亠仆亳亠 亳舒 仆舒仆亠 舒亳, 亢仂亶 从仂亟 舒于从亳 舒弍仂 Git/GitHub, Microsof VisualStudio 弌亠仄仆 亳亞仂亠于 8 亠于舒仍 2016亞. 3 / 13
- 5. 亳仆舒仄亳亠从亳 仂仄亳亠仄亶 从仂亟 string res = ""; for(i = 0; i < l; i++) res = "()" + res; use(res); 仗仗仂从亳仄舒亳 ("()")* 舒仄仄舒亳从舒 start ::= s s ::= LBR s RBR s s ::= 亠 舒亰弍仂舒 (SPPF) start_rule prod 2 s ! prod 0 prod 0 LBR s RBR eps LBR s RBR eps 弌亠仄仆 亳亞仂亠于 8 亠于舒仍 2016亞. 5 / 13
- 6. 舒亟舒舒: 仗亳仄亠仆亠仆亳亠 舒仆舒仍亳亰舒 仂从仂于 于舒亢亠仆亳亶 亟仍 JavaScript eval 丶亠仍: 舒仆仍亳 舒仆亟舒仆仂亞仂 eval 于 "弍亠亰仂仗舒仆亶" Martin Lester. Information Flow Analysis for a Dynamically Typed Functional Language with Staged Metaprogramming Martin Lester. Analysing Eval using Staged Metaprogramming 仍亠亟仂于舒亠仍从舒 亰舒亟舒舒: 亟亳仗仍仂仄, 仗弍仍亳从舒亳亳 舒亰弍亳于舒亠 仆舒 2 仗仂亟亰舒亟舒亳 仂仍亠仆亳亠 舒仗仗仂从亳仄舒亳亳 丐舒仆仍亳 SPPF 于 "弍亠亰仂仗舒仆亶 eval" 弌亠仄仆 亳亞仂亠于 8 亠于舒仍 2016亞. 6 / 13
- 7. 舒亟舒舒: 亳仗仂仍亰仂于舒仆亳亠 SPPF 于 舒弍舒从仆仂仄 亳仆舒从亳亠从仂仄 舒仆舒仍亳亰亠 弍舒从仆亶 亳仆舒从亳亠从亳亶 舒仆舒仍亳亰 仂亟亳仆 亳亰 仗仂亟仂亟仂于 从 舒仆舒仍亳亰 亟亳仆舒仄亳亠从亳 仂仄亳亠仄仂亞仂 从仂亟舒 K. G. Doh, H. Kim, D. A. Schmidt. Static Validation of Dynamically Generated HTML Documents Based on Abstract Parsing and Semantic Processing E. Verbitskaia, S. Grigorev, D. Avdyukhin. Relaxed Parsing of Regular Approximations of String-Embedded Languages 亠舒仍亳亰仂于舒 于亳仍亠仆亳亠 亠仄舒仆亳从亳 仗仂 舒礆 弌舒于仆亳 仆舒亳仄 仗仂亟仂亟仂仄 仄仂亢仆仂 仍亳 亳仗仂仍亰仂于舒 SPPF 亳仗仍仂仄, 仗弍仍亳从舒亳亳 弌亠仄仆 亳亞仂亠于 8 亠于舒仍 2016亞. 7 / 13
- 8. 弌亠亟于舒 亟仍 亠亳亳从舒仂仆仆仂亞仂 仗仂亞舒仄仄亳仂于舒仆亳 亳仍亳 F# + F* = ?
- 9. 弌亠亳亳从舒亳仂仆仆仂亠 仗仂亞舒仄仄亳仂于舒仆亳亠 F* (https://www.fstar-lang.org/tutorial/) Coq Agda ... val sort: l:list int -> Tot (m:list int{sorted m / (forall i. mem i l = mem i m)}) (decreases (length l)) let rec sort l = match l with | [] -> [] | pivot::tl -> let hi, lo = partition (cmp pivot) tl in let l = append (sort lo) (pivot::sort hi) in dedup l 弌亠仄仆 亳亞仂亠于 8 亠于舒仍 2016亞. 9 / 13
- 10. 舒亟舒舒: 仂弍亠亟亳仆亠仆亳亠 F# 亳 F* F# + F* = F#* 舒亠 亟仍 F#* 丐舒仆仍仂 亳亰 AST F# 于 AST F* 舒亰弍亳于舒亠 仆舒 仗仂亟亰舒亟舒亳 (亟仂 3 亠仍仂于亠从) 亳仗仍仂仄 (于 亰舒亟舒舒), 仗弍仍亳从舒亳亳 弌亠仄仆 亳亞仂亠于 8 亠于舒仍 2016亞. 10 / 13
- 11. 舒亟舒舒: 仗仂亟亟亠亢从舒 F#* 于 Microsoft Visual Studio 仂亟亟亠亢舒 于 仄仂亟亠仍亳 仗仂亠从舒, 亠亟舒从仂亠, 仂仍舒亟亳从亠 弌仂亰亟舒仆亳亠 舒亶仍仂于, 舒弍仍仂仆 仂亟于亠从舒 亳仆舒从亳舒 弌仂仂弍亠仆亳 仂弍 仂亳弍从舒, 仗仂亟于亠从舒 仂亳弍仂从 .... 舒亰弍亳于舒亠 仆舒 仗仂亟亰舒亟舒亳 (亟仂 4 亠仍仂于亠从) 亳仗仍仂仄 (于 亰舒亟舒舒), 仗弍仍亳从舒亳亳 弌亠仄仆 亳亞仂亠于 8 亠于舒仍 2016亞. 11 / 13
- 12. 舒亟舒舒: 仄亠亢磶从仂于仂亠 于亰舒亳仄仂亟亠亶于亳亠 F# 亳 F* 仗仂仍亰仂于舒 仆从亳亳, 仆舒仗亳舒仆仆亠 仆舒 F* 于 F#(.NET) 仗仂仍亰仂于舒 仆从亳亳, 仆舒仗亳舒仆仆亠 仆舒 F#(.NET) 于 F* 弌仂舒仆亳 亳仗亳亰舒亳/于于仂亟 亳仗仂于 舒亰弍亳于舒亠 仆舒 仗仂亟亰舒亟舒亳 (亟仂 2 亠仍仂于亠从) 亳仗仍仂仄 (于 亰舒亟舒舒), 仗弍仍亳从舒亳亳 弌亠仄仆 亳亞仂亠于 8 亠于舒仍 2016亞. 12 / 13
- 13. 仂仆舒从 仂舒: rsdpisuy@gmail.com 仂亟仆亶 从仂亟 YaccConstructor: https://github.com/YaccConstructor Google+ 仂仂弍亠于仂: https://goo.gl/DuPWkM 弌亠仄仆 亳亞仂亠于 8 亠于舒仍 2016亞. 13 / 13