基本信息
浏览量:60
职业迁徙
个人简介
DEGREES
Cornell University Ithaca, NY
Aug 2002 Ph.D. in Computer Science; Minor in Cognitive Studies
May 2000 M.S. in Computer Science
Moscow State University Moscow, Russia
Jun 1997 Diploma with Honors, Faculty of Mathematics and Mechanics, Division of Mathematics
Major: Mathematics, Applied Mathematics (Department of Mathematical Logic and Theory of Algorithms)
RESEARCH INTERESTS
Development, application, and theory of systems and tools for computer-aided programming language research and experimentation, computer-aided software engineering, and computer-aided reasoning and verification. Formal methods for reliable software design process. Development, application, and theory of interactive proof assistants and logical frameworks. Type theories, higher-order abstract syntax, and their applications.
RESEARCH EXPERIENCE
HRL Laboratories, LLC Malibu, CA
Since 8/2006 Research Staff Scientist
California Institute of Technology Pasadena, CA
9/2002-8/2006 Postdoctoral Scholar / Senior Postdoctoral Scholar with Prof. Jason Hickey
Research Projects: Computer-aided and formal software engineering based on the logical frameworks, including building reliable extensible compilers. Improving the software engineering capabilities of the MetaPRL formal toolkit. Foundations for practical syntax-based reasoning about properties of programming languages and languages with bindings, as well as for formal reasoning in the area of logical reflection in general. Formalizing the foundations of abstract algebra and number theory. Designing and implementing of the OMake build system. Designing serializability protocols for distributed filesystems.
Jul-Aug 2000 Visitor with Prof. Jason Hickey
MetaPRL Project
Since 1999 Coordinator and a Lead Developer. MetaPRL is a formal methods programming toolkit that can be used as a computer-aided software engineering tool. It is also an interactive tactic-based theorem prover. It also implements a logical framework that allows its users to specify and work with different logical theories and formalisms. Finally, MetaPRL is a basis for a programming language research, experimentation and meta-reasoning toolkit that is currently being developed.
Cornell University Ithaca, NY
9/1997-9/2002 Research Assistant with Prof. Robert Constable
Ph.D. Dissertation: Theory and Implementation of an Efficient Tactic-Based Logical Framework
Research Projects: Increased the logical speed of the MetaPRL system by two orders of magnitude. Came up with several methods of improving expressivity and making type theory formalization more usable in both automated and user-guided theorem proving.
Mar-Apr 1997 Visitor with Prof. Robert Constable
9/1992-6/1997 Moscow State University Moscow, Russia
9/1995-6/1997 Laboratory for Logical Problems in Computer Science (headed by Prof. Sergei Artemov)
9/1994-6/1997 Department of Mathematical Logic and Theory of Algorithms; Advisor: Prof. Alexander Razborov
May 1997 Diploma Thesis: Improving the Efficiency of NuPRL Proofs
研究兴趣
论文共 44 篇作者统计合作学者相似作者
按年份排序按引用量排序主题筛选期刊级别筛选合作者筛选合作机构筛选
时间
引用量
主题
期刊级别
合作者
合作机构
2023 IEEE INTERNATIONAL CONFERENCE ON ASSURED AUTONOMY, ICAApp.119-128, (2023)
mag(2015)
引用23浏览0引用
23
0
加载更多
作者统计
#Papers: 44
#Citation: 777
H-Index: 22
G-Index: 26
Sociability: 4
Diversity: 1
Activity: 1
合作学者
合作机构
D-Core
- 合作者
- 学生
- 导师
数据免责声明
页面数据均来自互联网公开来源、合作出版商和通过AI技术自动分析结果,我们不对页面数据的有效性、准确性、正确性、可靠性、完整性和及时性做出任何承诺和保证。若有疑问,可以通过电子邮件方式联系我们:report@aminer.cn