Programmeerimiskeelte semantika uurimisseminar

• Aine kood: MTAT.03.204
• Vastutavad õppejõud: Jevgeni Kabanov, Varmo Vene
• Ainepunkte: 5
• Konverentsi ajakava

• 08. 09., kell 10.15, Liivi 2, 405
  • Sissejuhatus.
  • Teemade tutvustus.
  • Ajakava paikapanek.
• 15. 09., kontakt e-mailiga
  • Igalt osalejalt tagasiside maili teel.
  • Teema peab olema valitud.
• 22. 09., kontakt e-mailiga
  • Teema lühisissejuhatus; sisukord ja kava; Lähtematerjali lühitutvustus.
  • Kirjalikus vormis ca 1-3 lk.
• 20. 10., kell 10.15, Liivi 2, 405
  • Vahekokkuvõte.
  • Vormistuslikud küsimused.
  • Esitada kirjatöö mustand (ca 2/3 ulatuses valmis).
  • Ettekanded (ca. 5 min, 1-2 slaidi) oma teema tutvustamiseks.
• 03. 11., kontakt e-mailiga
  • Artiklid hindamisele kaastudengitele.
  • Retsenseerimisvormid (Est, Eng).
• 17. 11., kontakt e-mailiga
  • Retsensioonide kokkukogumine, laialijagamine.
• 14. 12., kontakt e-mailiga
  • Lõppversioonide esitamine.
• 21.12., kell 11.15, Liivi 2-403, Konverents
  • Teemade kaupa grupeeritud-järjestatud loengud.
  • Iga ettekanne arvestuslikult 1 tund (40-45 + 10).

Programmianalüüs

• Terminator - programmide termineeruvus ja elusus
  • Terminator Research Project. http://research.microsoft.com/en-us/um/cambridge/projects/terminator/default.htm
  • Termination proofs for systems code. Byron Cook, Andreas Podelski, Andrey Rybalchenko. PLDI'06. http://research.microsoft.com/en-us/um/cambridge/projects/terminator/binreach.pdf
• "Shape" analüüs kasutades kolmeväärtuselist loogikat
  • TVLA - 3-Valued Logic Analysis Engine. http://www.cs.tau.ac.il/~tvla/
  • Parametric shape analysis via 3-valued logic. Mooly Sagiv, Thomas Reps, Reinhard Wilhelm. TOPLAS 24 (3): 217-298. http://www.math.tau.ac.il/~msagiv/toplas02.pdf
• CEGAR
  • Counterexample-Guided Abstraction Refinement for Symbolic Model Checking. Edmund Clarke, Orna Grumberg, Somesh Jha, Yuan Lu, Helmut Veith. JACM 50 (5): 752-794. http://www.cs.cmu.edu/~emc/papers/Papers%20In%20Refereed%20Journals/Counterexample-guided%20abstraction%20refinement.pdf
• Lineaaralgebral baseeruv programmianalüüs
  • Precise interprocedural analysis through linear algebra. Markus Müller-Olm and Helmut Seidl, POPL'04. http://portal.acm.org/citation.cfm?id=964001.964029
  • A Note on Karr's Algorithm. Markus Müller-Olm and Helmut Seidl, ICALP'04. http://www.springerlink.com/content/dyfrulyv6pdhpnul/

Varia

• Featherweight Verilog
  • Synthesizable high level hardware descriptions: using statically typed two-level languages to guarantee verilog synthesizability. Jennifer Gillenwater, Gregory Malecha, Cherif Salama, Angela Yun Zhu, Walid Taha, Jim Grundy, John O'Leary. PEPM'08. http://www.cs.rice.edu/~taha/publications/conference/pepm08.pdf
  • Static consistency checking for verilog wire interconnects: using dependent types to check the sanity of verilog descriptions. Cherif Salama, Gregory Malecha, Walid Taha, Jim Grundy, John O'Leary. (PEPM'09) http://www.cs.rice.edu/~taha/publications/conference/pepm09.pdf
• Tüübifunktsioonid
  • Fun with type functions. Oleg Kiselyov, Ken Shan, Simon Peyton Jones. 2010. http://haskell.org/haskellwiki/Simonpj/Talk:FunWithTypeFuns
• Omega
  • Languages of the Future. Tim Sheard. ACM SIGPLAN Notices, Dec. 2004. http://web.cecs.pdx.edu/~sheard/papers/LangOfTheFuture.ps
  • Generic Programming In Omega. Tim Sheard. 2006. http://web.cecs.pdx.edu/~sheard/papers/GenericNotes.ps
  • Programming In Omega. Tim Sheard, Nathan Linger. 2007. http://web.cecs.pdx.edu/~sheard/papers/SumSchNotes.ps
• Andmetüüpide "tuletised"
  • The Derivative of a Regular Type is its Type of One-Hole Contexts. Conor McBride. 2001. http://strictlypositive.org/diff.pdf
  • Clowns to the left of me, jokers to the right (pearl): dissecting data structures. Conor McBride. POPL'08. http://portal.acm.org/citation.cfm?id=1328897.1328474
• Ootevaba sünkroniseerimine
  • Wait-free synchronization. Maurice Herlihy. ACM Trans. Program. Lang. Syst. 13, 1 (January 1991). DOI: 10.1145/114005.102808
• Graafireduktsiooni abstraktne masin
  • The spineless tagless G-machine. S. Peyton Jones, J. Salkild. FPCA'89. DOI: 10.1145/99370.99385
  • The spineless tagless G-machine. S. Peyton Jones. JFP 2, 2 (April 1992). DOI: 10.1017/S0956796800000319
• Sõltuvate tüüpidega objektid
  • A Nominal Theory of Objects with Dependent Types. Martin Odersky, Vincent Cremet, Christine Röckl, Matthias Zenger. ECOOP 2003. DOI: 10.1007/978-3-540-45070-2_10

• I. Parberry, "A Guide for New Referees in Theoretical Computer Science". Information and Computation, Vol. 112, No. 1, pp. 96-116, 1994.
• Vormistusjuhend (J.Vilo)
• 2003 a. J.Vilo organiseeritud "Andmekaevanduse uurimisseminari" veebileht
• Programmeerimiskeelte semantika uurimisseminar (2009 sügis)
• Programmeerimiskeelte semantika uurimisseminar (2008 sügis)