Download CV: PDF Version, Postscript Version 
Aleksey Nogin  Curriculum Vitae 


Citizenship:  USA  
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 computeraided programming language research and experimentation, computeraided software engineering, and computeraided reasoning and verification. Formal methods for reliable software design process. Development, application, and theory of interactive proof assistants and logical frameworks. Type theories, higherorder 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/20028/2006  Postdoctoral Scholar / Senior Postdoctoral Scholar with Prof. Jason Hickey  
Research Projects: Computeraided 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 syntaxbased 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.  
JulAug 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 computeraided software engineering tool. It is also an interactive tacticbased 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 metareasoning toolkit that is currently being developed.  
Cornell University  Ithaca, NY  
9/19979/2002  Research Assistant with Prof. Robert Constable  
Ph.D. Dissertation: Theory and Implementation of an Efficient TacticBased 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 userguided theorem proving.  
MarApr 1997  Visitor with Prof. Robert Constable  
9/19926/1997  Moscow State University  Moscow, Russia  
9/19956/1997  Laboratory for Logical Problems in Computer Science (headed by Prof. Sergei Artemov)  
9/19946/1997  Department of Mathematical Logic and Theory of Algorithms; Advisor: Prof. Alexander Razborov  
May 1997  Diploma Thesis: Improving the Efficiency of NuPRL Proofs  
RELATED EXPERIENCE  
Participated in creation of three successful grant applications:  
A recent MetaPRLbased grant by Laboratory for Computational Methods at Moscow State University (approximately 30 menyears worth of funding);  
NSF grant 0313354 “ITR: Reliable Distributed Programming with Speculations”;  
ONR/MURI grant N000140110765 “Building Interactive Digital Libraries of Formal Algorithmic Knowledge”.  
Coorganized a daylong tutorial “Introduction to MetaPRL Theorem Prover” given at the 16th International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2003).  
TEACHING EXPERIENCE  
California Institute of Technology  Pasadena, CA  
Fall 2005  Creator and Instructor, undergraduate course LanguageBased Security.  
June 2004  Creator and Instructor, course Introduction into formal computeraided reasoning and the MetaPRL theorem prover, North American Summer School in Logic, Language and Information (NASSLI) 2004 at UCLA.  
Winter 2004  Creator and Instructor, graduate / advanced undergraduate course Programing Language Semantics.  
Spring 2003  Creator and Instructor, graduate / advanced undergraduate MetaPRLbased course Type Theory and Formal Methods.  
Cornell University  Ithaca, NY  
Spring 2002  TA, undergraduate course Structure and Interpretation of Computer Programs.  
Fall 2000  Instructor, undergraduate course Introduction to Unix.  
Spring 1998  TA, undergraduate course Structure and Interpretation of Computer Programs.  
Fall 1997  TA, undergraduate course Introduction to Theory of Computing (Honors).  
PUBLICATIONS  
2006 
Jason Hickey, Aleksey Nogin, Xin Yu, and Alexei Kopylov
Mechanized metareasoning using a hybrid HOAS/de Bruijn representation and reflection. In John H. Reppy and Julia L. Lawall, editors, Proceedings of the 11th ACM SIGPLAN International Conference on Functional Programming, ICFP 2006, pages 172–183. ACM, 2006. Jason Hickey and Aleksey Nogin. OMake: Designing a scalable build process. In Luciano Baresi and Reiko Heckel, editors, Fundamental Approaches to Software Engineering, 9th International Conference, FASE 2006, volume 3922 of Lecture Notes in Computer Science, pages 63–78. Springer, 2006. An extended version is available as California Institute of Technology technical report CaltechCSTR:2006.001. Aleksey Nogin and Alexei Kopylov. Formalizing type operations using the “Image” type constructor. In Proceedings of the 13th Workshop on Logic, Language, Information and Computation (WoLLIC 2006), volume 165 of Electronic Notes in Theoretical Computer Science, pages 121–132. Elsevier, 2006. Extended version was submitted to Information and Computation Journal. Jason Hickey, Aleksey Nogin, Xin Yu, and Alexei Kopylov Practical reflection for sequent logics. In Proceedings of the International Workshop on Logical Frameworks and MetaLanguages: Theory and Practice (LFMTP'06), Electronic Notes in Theoretical Computer Science, 2006. Jason Hickey and Aleksey Nogin. Formal Compiler Construction in a Logical Framework. HigherOrder and Symbolic Computation, 19(2–3):197–230, September 2006.  
2005 
Aleksey Nogin, Alexei Kopylov, Xin Yu, and Jason Hickey.
A Computational Approach to Reflective MetaReasoning about Languages with Bindings. In MERLIN '05: Proceedings of the 3rd ACM SIGPLAN workshop on Mechanized reasoning about languages with variable binding, pages 2–12. ACM Press, 2005. An extended version is available as California Institute of Technology technical report CaltechCSTR:2005.003.  
2004 
Nathaniel Gray, Jason Hickey, Aleksey Nogin, and Cristian Tapus.
Building Extensible Compilers in a Formal Framework. A Formal Framework User's Perspective. In Konrad Slind, editor, Emerging Trends. Proceedings of the 17th International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2004), pages 57–70. University of Utah, 2004. Cristian Tapus, Aleksey Nogin, Jason Hickey, and Jerome White. A Simple Serializability Mechanism for a Distributed Objects System. In David A. Bader and Ashfaq A. Khokhar, editors, Proceedings of the 17th International Conference on Parallel and Distributed Computing Systems (PDCS2004). International Society for Computers and Their Applications (ISCA), 2004. Jason Hickey and Aleksey Nogin. Extensible Hierarchical Tactic Construction in a Logical Framework. In Konrad Slind, Annette Bunker, and Ganesh Gopalakrishnan, editors, Proceedings of the 17th International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2004), volume 3223 of Lecture Notes in Computer Science, pages 136–151. SpringerVerlag, 2004.  
2003 
Jason Hickey, Aleksey Nogin, Robert L. Constable, Brian E. Aydemir, Eli
Barzilay, Yegor Bryukhov, Richard Eaton, Adam Granicz, Alexei Kopylov,
Christoph Kreitz, Vladimir N. Krupski, Lori Lorigo, Stephan Schmitt, Carl
Witty, and Xin Yu.
MetaPRL — A Modular Logical Environment. In David Basin and Burkhart Wolff, editors, Proceedings of the 16th International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2003), volume 2758 of Lecture Notes in Computer Science, pages 287–303. SpringerVerlag, 2003. Jason Hickey, Aleksey Nogin, Adam Granicz, and Brian Aydemir. Compiler Implementation in a Formal Logical Framework. In Proceedings of the 2003 workshop on Mechanized reasoning about languages with variable binding, pages 1–13. ACM Press, 2003. Xin Yu, Aleksey Nogin, Alexei Kopylov, and Jason Hickey. Formalizing Abstract Algebra in Type Theory with Dependent Records. In David Basin and Burkhart Wolff, editors, 16th International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2003). Emerging Trends Proceedings, pages 13–27. Universität Freiburg, 2003. Yegor Bryukhov, Alexei Kopylov, Vladimir Krupski, and Aleksey Nogin. Implementing and Automating Basic Number Theory in MetaPRL Proof Assistant. In David Basin and Burkhart Wolff, editors, 16th International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2003). Emerging Trends Proceedings, pages 29–39. Universität Freiburg, 2003. Nathaniel Gray, Cristian Tapus, Aleksey Nogin, and Jason Hickey. Building Reliable Compilers with a Formal Methods Framework. In Dr. Indrakshi Ray, editor, The 14th International Symposium on Software Reliability Engineering (ISSRE 2003). Supplementary Proceeding, pages 319–320. Chillarege Press, 2003.  
2002 
Aleksey Nogin.
Theory and Implementation of an Efficient TacticBased Logical Framework. Ph.D. Thesis, Cornell University. August 2002. Aleksey Nogin. Quotient Types: A Modular Approach. In Victor A. Carreño, Cézar A. Muñoz, and Sophiène Tahar, editors, Proceedings of the 15th International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2002), volume 2410 of Lecture Notes in Computer Science, pages 263–280. SpringerVerlag, 2002. Aleksey Nogin and Jason Hickey. Sequent Schema for Derived Rules. In Victor A. Carreño, Cézar A. Muñoz, and Sophiène Tahar, editors, Proceedings of the 15th International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2002), volume 2410 of Lecture Notes in Computer Science, pages 281–297. SpringerVerlag, 2002.  
2001 
Alexei Kopylov and Aleksey Nogin.
Markov's principle for propositional type theory. In L. Fribourg, editor, Computer Science Logic, Proceedings of the 10th Annual Conference of the EACSL, volume 2142 of Lecture Notes in Computer Science, pages 570584. SpringerVerlag, 2001. Stephan Schmitt, Lori Lorigo, Christoph Kreitz, and Aleksey Nogin. Jprover: Integrating connectionbased theorem proving into interactive proof assistants. In International Joint Conference on Automated Reasoning, volume 2083 of Lecture Notes in Artificial Intelligence, pages 421426. SpringerVerlag, 2001.  
2000 
Jason J. Hickey and Aleksey Nogin.
Fast tacticbased theorem proving. In J. Harrison and M. Aagaard, editors, Theorem Proving in Higher Order Logics: 13th International Conference, TPHOLs 2000, volume 1869 of Lecture Notes in Computer Science, pages 252266. SpringerVerlag, 2000. Aleksey Nogin. Writing constructive proofs yielding efficient extracted programs. In Didier Galmiche, editor, Proceedings of the Workshop on TypeTheoretic Languages: Proof Search and Semantics, volume 37 of Electronic Notes in Theoretical Computer Science. Elsevier Science Publishers, 2000  
1997 
Aleksey Nogin.
Improving the efficiency of NuPRL proofs. Department of Computer Science TR971643, Cornell University, August 1997.  
1995 
Aleksey Nogin.
On Horn interpolation in linear logic. Mathematical Logic and Theoretical Computer Science Prepublication Series 199511, Steklov Mathematical Institute, April 1995. In Russian.  
ONLINE PUBLICATIONS  
Jason Hickey, Aleksey Nogin, et al.
OMake Home Page. http://omake.metaprl.org/ Jason Hickey, Aleksey Nogin, Alexei Kopylov, et al. MetaPRL Home Page. http://metaprl.org/ Jason Hickey, Brian Aydemir, Yegor Bryukhov, Alexei Kopylov, Aleksey Nogin, and Xin Yu. A listing of MetaPRL theories. http://metaprl.org/theories.pdf Jason Hickey, Nathaniel Gray, Aleksey Nogin, Cristian Tapus, and Xin Yu. Introduction to MetaPRL Theorem Prover. Tutorial: Implementing FOL in MetaPRL. http://files.metaprl.org/papers/tutorial1.pdf Jason Hickey and Aleksey Nogin. MetaPRL System Description http://metaprl.org/system/default.html Jason Hickey, Aleksey Nogin and Alexei Kopylov. MetaPRL User Guide. http://metaprl.org/userguide/default.html Aleksey Nogin and Vladimir Krupski. MetaPRL Developer Guide. http://metaprl.org/developerguide/default.html  
TALKS  
Sep 2005  3rd ACM SIGPLAN workshop on Mechanized reasoning about languages with variable binding, Tallinn, Estonia  
Mar 2005  CS Colloquium, Purdue University, West Lafayette, IN  
Oct 2004  Microsoft Research, Redmond, WA  
Sep 2004  Theorem Proving in Higher Order Logics, 17th International Conference, Park City, UT  
Sep 2003  Seminar Logical Problems in Computer Science, Department of Mathematical Logic and Theory of Algorithms, Faculty of Mathematics and Mechanics, Moscow State University, Moscow, Russia  
Apr 2003  Microsoft Research, Redmond, WA  
Dec 2002  City University of New York Graduate Center, Computer Science Colloquium  
Aug 2002  Theorem Proving in Higher Order Logics, 15th International Conference, Hampton, VA, two talks  
Sep 2001  Computer Science Logic, 10th Annual Conference of the EACSL, Paris, France  
Sep 2001  Logic Seminar Series, Department of Informatics of Saarland University and MPI Institute, Saarbrücken, Germany  
Aug 2000  Theorem Proving in Higher Order Logics, 13th International Conference, Portland, OR  
Jun 2000  Workshop on TypeTheoretic Languages: Proof Search and Semantics, Pittsburgh, PA  
Mar 2000  Seminar Logical Problems in Computer Science, Department of Mathematical Logic and Theory of Algorithms, Faculty of Mathematics and Mechanics, Moscow State University, Moscow, Russia  
ACADEMIC AND COMMUNITY SERVICE  
20002006  Helped to set up and administer a 16x2node cluster for Jason Hickey's Mojave Group at Caltech  
Since 1997  Contributor to Open Source projects, including OCaml, Mozilla and Red Hat Linux/Fedora Project  
19972002  Set up and administered a departmentwide CVS server. Administered Linux servers for the Cornell PRL group  
19951997  Set up and administered network, mail, and dialup servers for the Youth Scientific Creativity Center 
Last update: Sunday, January 28, 2007