Bojan Petrovic edited this page Apr 23, 2015 · 27 revisions

wiki logo

Wiki za radionicu Coq-a prema kursu "Software Foundations" (CIS 500) Bendžamina Pirsa

Beleške sa radionice

Pastebin

Za vreme radionice, sadržaj fajla koji odgovara poglavlju na kojem radimo biće ažuriran na na ix.io pastebinu (http://ix.io/user/bojan). Nakon završene sesije, svi fajlovi će biti komitovani u repo.

  1. Basics.v
  2. Lists.v
  3. Poly.v
  4. Prop.v
  5. Logic.v
  6. SfLib.v
  7. Imp.v
  8. Hoare.v

Linkovi

Web sadržaji

Softver

  • Coq - glavna strana Coq proof assistanta
  • Proof General - Emacs front-end za Coq i druge proof sisteme

#Literatura

Coq

  • Bertot, Yves, Castéran, Pierre (2004). Interactive Theorem Proving and Program Development: Coq'Art: The Calculus of Inductive Constructions - detaljan priručnik za Coq
  • Bruno Barras, Benjamin Werner (1997). Coq in Coq - formalizacija računa induktivnih konstrukcija u samom Coq-u

Logika

Teorija tipova

  • Per Martin-Löf (1984). Intuitionistic Type Theory - osnovni tekst
  • Johan Georg Granström (2011). Treatise on Intuitionistic Type Theory - Uvod u intuicionističku teoriju tipova sa zanimljivim multidisciplinarnim logičko-filozofskim pristupom; mnoštvo istorijskih referenci, od Pitagore pa na ovamo.

Formalna verifikacija

Citati

After having devoted a considerable number of years of my scientific life to clarifying the programmer's task, with the aim of making it intellectually better manageable, I found this effort at clarification to my amazement (and annoyance) repeatedly rewarded by the accusation that "I had made programming difficult". But the difficulty has always been there, and only by making it visible can we hope to become able to design programs with a high confidence level, rather than "smearing code", i.e., producing texts with the status of hardly supported conjectures that wait to be killed by the first counterexample. None of the programs in this monograph, needless to say, has been tested on a machine.

Edsger Dijkstra (1976). "A Discipline of Programming"

Ten years ago, researchers into formal methods (and I was the most mistaken among them) predicted that the programming world would embrace with gratitude every assistance promised by formalisation to solve the problems of reliability that arise when programs get large and more safety-critical. Programs have now got very large and very critical -- well beyond the scale which can be comfortably tackled by formal methods. There have been many problems and failures, but these have nearly always been attributable to inadequate analysis of requirements or inadequate management control. It has turned out that the world just does not suffer significantly from the kind of problem that our research was originally intended to solve.

Hoare, C. A. R. (1996). "Unification of Theories: A Challenge for Computing Science".

Coq u "stvarnom svetu"

Wouter Swierstra (2012). xmonad in Coq - izveštaj o iskustvu ručnog prevođenja StackSet.hs modula xmonad window managera u Coq, i u ekstrakciji Haskell koda u obrnutom smeru.

You can’t perform that action at this time.
You signed in with another tab or window. Reload to refresh your session. You signed out in another tab or window. Reload to refresh your session.
Press h to open a hovercard with more details.