Eugene Kornykhin (Евгений Корныхин)
Contact:
 Department of System Programming
 Faculty of Computational Mathematics and Cybernatics
 Lomonosov Moscow State University
 Leninskie gory, bld. 52, room 718
 Moscow 119992 GSP2, Russia
 Email:
 Mobile: +7 (903) 1471623
 Office: +7 (495) 9391877
 Twitter: kornevgen
 Истина: kornevgen
Teaching

Introduction to functional programming (fall 2011) at Lomonosov Moscow State University (in Russian)
 slides:
welcome (pdf),
part11 (pdf),
part12 (pdf),
part13 (pdf),
part21 (pdf),
part22 (pdf),
part23 (pdf),
part31 (pdf)
, part32 (pdf)
, part33 (pdf)
 Try Scheme in your browser! (you will use GNU intepreter for Scheme).
 Download Scheme (Racket):
Windows x86,
Windows x64,
Ubuntu x86,
Debian squeeze x64,
other links
 Expressiononly style conventions (without if statement)
 all formal parameters are const
 no global variables and fields
 no functions with `void' return type
 all local variables are const
 only allowed statement is a return statement
 only one return in function
 Expressiononly style conventions (with if statement)
 all formal parameters are const
 no global variables and fields
 no functions with `void' return type
 all local variables are const
 each ifstatement has elsebranch
 each branch of ifstatement ends with return statement
 each switchstatement has defaultbranch
 no goto, while, for, dowhile statements
 no "expression statements" (f.e., "x;", "f(x);" statement)
 no unreachable code
 functional lists:
fplists.h,
fplists.cpp
 advanced expressiononly style trainings:
 long arithmetic (addition, subtraction)
 long multiplication in columns (idea for the solution)
 Karatsuba multiplication (idea1, idea2)
 the path in the maze problem solutions (don't look at them before the seminar):
variant1,
variant2,
variant3,
variant4
 Doctor
 homeworks ##13
 homework #1.1 (rewrite according to expressiononly style in C++):
00.c,
01.c,
02.c,
03.c
 homework #1.2 (implement according to expressiononly style in C++):
 for a given natural number, return its maximal prime divisor
 for a given natural number, return production of its maximal prime divisor and premaximal prime divisor, or 1, if a given number is prime
 for a given natural number, return the closest upper prime number for it
 homework #2.1 (implement according to expressiononly style in C++):
 for a given ordered list and a number, insert this number to the list preserving order
 for a given list of numbers and a number from this list, return count of its occurences in this list
 for a given list of numbers, return its reversed version
 for a given list of numbers, return sum of its items
 for given two ordered lists of numbers, merge theirs (ordered list with items from both lists)
 homework #3.1 (implement according to expressiononly style in C++ using tail recursion):
 for a given ordered list and a number, insert this number to the list preserving order
 for a given list of numbers and a number from this list, return count of its occurences in this list
 for a given list of numbers, return its reversed version
 for a given list of numbers, return sum of its items
 for given two ordered lists of numbers, merge theirs (ordered list with items from both lists)
 for a given list of numbers, return another list with the same items but without duplicates (order doesn't matter)
 for given two lists of numbers, return theirs common items without duplicates (order doesn't matter), source lists don't contain duplicates
 for given two lists of numbers, return theirs common items without duplicates (order doesn't matter), source lists may contain duplicates
 for a given list of numbers, return maximal sum of pair of different items from this list
 Genetic programming: variants, additional slides, about visualization.

Software formal specification and verification (fall 2011) at Lomonosov Moscow State University (in Russian)
 Dafny docs:
tutorials,
quick reference,
paper
 Dafny binaries
(prerequisites: Microsoft Windows, Microsoft .NET Framework)
 Dafny trainings: controlflow, numbers:
1,
2,
3,
4,
5,
6,
7,
8,
9,
10,
11,
12,
13,
14!
 Dafny trainings: arrays, quantifiers :
1,
2,
3,
4,
5,
6,
7,
8,
9,
10,
11,
12,
13,
14
 Dafny trainings:
sets,
sequences :
1,
2,
3,
4,
5,
6,
7,
8,
9,
10,
11,
12,
13,
14,
15,
16
 Dafny trainings: lemmas,
induction :
1,
2,
3,
4,
5,
6,
7,
8,
9,
10,
11,
12,
13,
14,
15,
16,
17
 Dafny trainings: matching triggers, abstraction :
1,
2,
3,
4,
5,
6,
7,
8,
9,
10
 Dafny trainings: dynamic frames :
*
*
*
*,
*
 Dafny trainings: algebraic data types :
*,
*,
*,
*,
*
 PVS docs:
Introduction to PVS
, quick reference
, prover guide (list of commands)
, language reference (PVS specification language)
 PVS trainings: propositional, predicate, and equational logic :
 prove all lemmas from here
 PVS trainings: induction (prove all lemmas from files) :
sum_why.pvs
, sum2_why.pvs
, three.pvs
, sum_square.pvs
, divides.pvs
, sum3_why.pvs