Podstawy języków programowania w systemie Coq
Terminarz
|
Plan zajęć
| Data |
Temat |
Podręcznik |
Kod |
Literatura dodatkowa |
Zadania |
| 08.10.2014 |
Organizacja przedmiotu
Podstawy programowania funkcyjnego w Coqu
|
Basics
|
Basics.v
|
|
factorial, blt_nat, boolean_functions, and_eq_orb, binary |
| 15.10.2014 |
Indukcja
Listy
|
Induction
Lists
|
Induction.v
Lists.v
| |
basic_induction, mult_comm, binary_commute, list_exercises, list_design |
| 22.10.2014 |
Polimorfizm i funkcje wyższego rzędu
|
Poly
|
Poly.v
|
|
mumble_grumble, currying, map_rev, override_neq, fold_map |
| 29.10.2014 |
Więcej na temat taktyk (m. in. apply, inversion, generalize dependent)
|
MoreCoq
|
MoreCoq.v
|
|
rev_exercise1, plus_n_n_injective, gen_dep_practice_more, double_induction, combine_split |
| 05.11.2014 |
Logika w Coqu
|
Logic
|
Logic.v
|
|
and_assoc, or_distributes_over_and_2, bool_prop, contrapositive, excluded_middle_irrefutable |
| 12.11.2014 |
Predykaty indukcyjne
Termy jako dowody
|
Prop
MoreLogic
|
Prop.v
MoreLogic.v
|
|
ev_sum, b_timesm, beautiful_gorgeous, palindromes, combine_odd_even, not_exists_dist, filter_challenge |
| 19.11.2014 |
Modelowy język imperatywny IMP
|
Imp
|
Imp.v
|
|
optimize_0plus_b, optimizer, bevalR, update_same, update_permute |
| 26.11.2014 |
Modelowy język imperatywny IMP, c.d.
Równoważność programów
|
Imp
Equiv
|
Imp.v
Equiv.v
|
|
XtimesYinZ_spec, loop_never_stops,
stack_compiler, stack_compiler_correct,
swap_if_branches, CIf_congruence,
fold_constants_com_sound |
| 10.12.2014 |
Równoważność programów, c.d.
Logika Hoare'a
|
Equiv
Hoare
|
Equiv.v
Hoare.v
|
|
optimize_0plus, better_subst_equiv, inequiv_exercise
|
| 17.12.2014 |
Logika Hoare'a, c.d.
|
Hoare
Hoare2
|
Hoare.v
Hoare2.v
|
|
swap_exercise, if1_hoare, slow_assignment,
two_loops, hoare_asgn_weakest, slow_assignment_dec
|
| 14.01.2015 |
Logika Hoare'a, c.d.
Semantyka małych kroków
|
HoareAsLogic
Smallstep
|
HoareAsLogic.v
Smallstep.v
|
|
hoare_proof_complete, redo_determinism,
normal_forms_unique, eval__multistep, step__eval,
multistep__eval
|
| 21.01.2015 |
Automatyzacja dowodów
Typy
|
Auto
Types
|
Auto.v
Types.v
|
|
some_term_is_stuck, value_is_nf, finish_progress,
finish_preservation, prog_pres_bigstep
|
| 28.01.2015 |
Rachunek lambda z typami prostymi jako modelowy język programowania
|
Stlc
StlcProp
|
Stlc.v
StlcProp.v
|
|
substi, typing_nonexample_3, progress_from_term_ind,
subject_expansion_stlc, types_unique
|
| 04.02.2015 |
Algorytm sprawdzania typu (weryfikacja, ekstrakcja programu z dowodu rozstrzygalności)
Twierdzenie o normalizacji w rachunku lambda z typami prostymi (relacje logiczne)
|
Typechecking
Norm
|
Typechecking.v
Norm.v
|
|
|
|
Prace domowe Rozwiązania zadań należy przesłać na
adres e-mail prowadzącego w nieprzekraczalnym terminie
zwrotu podanym dla każdej pracy domowej. Wszystkie
rozwiązania powinny znajdować się w jednym pliku o nazwie
Assignment_Nr_Imię_Nazwisko.v, którego szablon
stanowi plik Assignment_Nr.v, gdzie Nr to
numer pracy domowej, a Imię i Nazwisko, to
imię i nazwisko autora rozwiązań.
Przesłany plik musi przejść kompilację
poleceniem coqc by został oceniony -- proszę używać
komendy Admitted w razie gdy rozwiązanie jest
niepełne oraz założyć, że włączane w szablonie pliki za
pomocą komendy Require są identyczne z tymi na
stronie podręcznika i że są to jedyne pliki wymagane przez
plik z rozwiązaniami. Można korzystać z biblioteki
standardowej w zakresie, który nie przekreśla sensu zadania.
Przesłane rozwiązania powinny być opracowane samodzielnie,
co zostanie sprawdzone ze szczególną uwagą. Niepełne
rozwiązania również będą punktowane.
|