TBD
Date — Lead by — Paper citation
Jan 2019 — — (Organizational meeting)
Date — Lead by — Paper citation
15 Jun 2016 — Arthur — Oliveira, Bruno C. d. S.; Cook, William R. Extensibility for the Masses: Practical Extensibility with Object Algebras. In: ECOOP 2012 – Object-Oriented Programming Volume 7313 of the series Lecture Notes in Computer Science. Springer Berlin Heidelberg; 2012. p. 2–22. doi: 10.1007/978-3-642-31057-7_2. Available from: http://dx.doi.org.ezproxy.lib.utexas.edu/10.1007/978-3-642-31057-7_2
06 Jul 2016 — Jia — Reps, Thomas. Program analysis via graph reachability. Information and Software Technology. 1998; 40(11–12):701–726. doi:10.1016/S0950-5849(98)00093-7. Available from: http://dx.doi.org.ezproxy.lib.utexas.edu/10.1016/S0950-5849(98)00093-7
13 Jul 2016 — John —
Date — Lead by — Paper citation
02 Sep 2015 — Loc — Lal, Akash; Qadeer, Shaz. DAG inlining: a decision procedure for reachability-modulo-theories in hierarchical programs. In: Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI ’15). ACM; 2015. p. 280–290. doi: 10.1145/2737924.2737987. Available from: http://dx.doi.org.ezproxy.lib.utexas.edu/10.1145/2737924.2737987
09 Sep 2015 — Arthur — Kjolstad, Fredrik; Kamil, Shoaib; Ragan-Kelley, Jonathan; Levin, David I.W.; Sueda, Shinjiro; Chen, Desai; Vouga, Etienne; Kaufman, Danny M.; Kanwar, Gurtej; Matusik, Wojciech; Amarasinghe, Saman. Simit: A Language for Physical Simulation. Cambridge (MA): Massachusetts Institute of Technology, Computer Science and Artificial Intelligence Laboratory; 2015. Report No.: MIT-CSAIL-TR-2015-017. Available from: http://hdl.handle.net/1721.1/97075
16 Sep 2015 — John — Bocchino, Jr., Robert L.; Adve, Vikram S; Dig, Danny; Adve, Sarita V; Heumann, Stephen; Komuravelli, Rakesh; Overbey, Jeffrey; Simmons, Patrick; Sung, Hyojin; Vakilian, Mohsen. A type and effect system for deterministic parallel Java. In: Proceedings of the 24th ACM SIGPLAN Conference on Object Oriented Programming Systems Languages and Applications (OOPSLA '09). ACM; 2015. p. 97–116. doi: 10.1145/1640089.1640097. Available from: http://doi.acm.org.ezproxy.lib.utexas.edu/10.1145/1640089.1640097
30 Sep 2015 — Arthur — Yakushev, Alexey Rodriguez; Holdermans, Stefan; Löh, Andres; Jeuring, Johan. Generic programming with fixed points for mutually recursive datatypes. In Proceedings of the 14th ACM SIGPLAN international conference on Functional programming (ICFP '09). ACM; 2009. P. 233-244. doi: 10.1145/1596550.1596585. Available from: http://doi.acm.org.ezproxy.lib.utexas.edu/10.1145/1596550.1596585
14 Oct 2015 — John — Park, Daejun; Stefănescu, Andrei; Roşu, Grigore. KJS: A complete formal semantics of JavaScript. In: Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI ’15). ACM; 2015. p. 346–356. doi: 10.1145/2737924.2737991. Available from: http://doi.acm.org.ezproxy.lib.utexas.edu/10.1145/2737924.2737991
21 Oct 2015 — Ashay — Samak, Malavika; Ramanathan, Murali Krishna; Jagannathan, Suresh. Synthesizing racy tests. In: Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI ’15). ACM; 2015. p. 175–185. doi: 10.1145/2737924.2737998. Available from: http://doi.acm.org.ezproxy.lib.utexas.edu/10.1145/2737924.2737998
28 Oct 2015 — Arthur — Apel, Sven; Kastner, Christian; Lengauer, Christian. FEATUREHOUSE: Language-independent, automated software composition. In: Proceedings of the 31st International Conference on Software Engineering (ICSE '09). IEEE Computer Society, Washington, DC, USA, 221-231. dui: 10.1109/ICSE.2009.5070523. Available from: http://dx.doi.org.ezproxy.lib.utexas.edu/10.1109/ICSE.2009.5070523
04 Nov 2015 — Jia — Might, Matthew; Smaragdakis, Yannis; Van Horn, David. Resolving and exploiting the k-CFA paradox: Illuminating functional vs. object-oriented program analysis. In: Proceedings of the 31st ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI '10). ACM; 2010. p. 305–315. doi: 10.1145/1806596.1806631. Available from: http://doi.acm.org.ezproxy.lib.utexas.edu/10.1145/1806596.1806631
11 Nov 2015 — Loc — Kulkarni, Milind; Pingali, Keshav; Walter, Bruce; Ramanarayanan, Ganesh; Bala, Kavita; Chew, L. Paul. Optimistic parallelism requires abstractions. In: Proceedings of the 2007 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI '07). ACM; 2007. p. 211–222. doi: 10.1145/1250734.1250759. Available from: http://doi.acm.org.ezproxy.lib.utexas.edu/10.1145/1250734.1250759
No date yet — — Canning, Peter; Cook, William; Hill, Walter; Olthoff, Walter; Mitchell, John C. F-bounded polymorphism for object-oriented programming. In: Proceedings of the Fourth International Conference on Functional Programming Languages and Computer Architecture (FPCA '89). ACM; 1989. p. 273-280. doi: 10.1145/99370.99392. Available from: http://doi.acm.org.ezproxy.lib.utexas.edu/10.1145/99370.99392
Typing object systems
Gradual typing
Date — Lead by — Paper citation
20 Jan 2015 — — (Organizational meeting)
27 Jan 2015 — Arthur — Cremet, Vincent; Garillot, François; Lenglet, Sergueï; Odersky, Martin. A core calculus for Scala type checking. In: Mathematical Foundations of Computer Science 2006. (Lecture Notes in Computer Science, vol. 4162). Springer; 2006. p. 1–23. Available from: http://link.springer.com.ezproxy.lib.utexas.edu/chapter/10.1007/11821069_1
03 Feb 2015 — Barry — Pearce, David J. Sound and complete flow typing with unions, intersections and negations. In: Proceedings of the 14th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI '13). Springer; 2013. p. 335-354. Available from: http://link.springer.com.ezproxy.lib.utexas.edu/chapter/10.1007/978-3-642-35873-9_21
10 Feb 2015 — Arthur — Igarashi, Atsushi; Pierce, Benjamin C. On inner classes. Information and Computation. 2002 Aug; 177(1): 56–89. Available from: http://www.sciencedirect.com.ezproxy.lib.utexas.edu/science/article/pii/S0890540102930920
17 Feb 2015 — Barry — Cook, Byron; Podelski, Andreas; Rybalchenko, Andrey. Termination proofs for systems code. In: Proceedings of the 2006 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI '06). ACM; 2006. p. 415–426. Available from: http://doi.acm.org.ezproxy.lib.utexas.edu/10.1145/1133981.1134029
03 Mar 2015 — John — Dillig, Işıl; Dillig, Thomas; Aiken, Alex. Automated error diagnosis using abductive inference. In: Proceedings of the 33rd ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI ’12). ACM; 2012. p. 181–192. doi: 10.1145/2254064.2254087. Available from: http://doi.acm.org.ezproxy.lib.utexas.edu/10.1145/2254064.2254087
10 Mar 2015 — John — Ibraheem, Husain; Schmidt, David A. Adapting big-step semantics to small-step style: Coinductive interpretations and “higher-order” derivations. Paper presented at: Second Workshop on Higher Order Operational Techniques in Semantics (HOOTS II); 1997 Dec 8–11; Stanford, CA. Author's version available from: http://people.cis.ksu.edu/~schmidt/papers/bsss.ps.gz
24 Mar 2015 — Barry — Foster, Simon; Struth, Georg. Integrating an automated theorem prover into Agda. In: NASA Formal Methods: Third International Symposium (NFM 2011). (Lecture Notes in Computer Science Volume, vol. 6617). Springer; 2011. p. 116-130. Available from: http://link.springer.com.ezproxy.lib.utexas.edu/chapter/10.1007/978-3-642-20398-5_10
31 Mar 2015 — Loc — Berger, Emery D.; Zorn, Benjamin G.. DieHard: Probabilistic memory safety for unsafe languages. In: Proceedings of the 2006 ACM SIGPLAN conference on Programming language design and implementation (PLDI '06). ACM; 2006. p. 158–168. http://doi.acm.org.ezproxy.lib.utexas.edu/10.1145/1133981.1134000
07 Apr 2015 — Loc — Zee, Karen; Kuncak, Viktor; Rinard, Martin. Full functional verification of linked data structures. In Proceedings of the 2008 ACM SIGPLAN conference on Programming language design and implementation (PLDI '08). ACM; 2008. p. 349–361. http://doi.acm.org.ezproxy.lib.utexas.edu/10.1145/1375581.1375624
14 Apr 2015 — Barry — Castagna, Giuseppe; Nguyen, Kim; Xu, Zhiwu; Im, Hyeonseung; Lenglet, Sergueï; Padovani, Luca. Polymorphic functions with set-theoretic types: part 1: syntax, semantics, and evaluation. In Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL '14). ACM; 2014. p. 5–17. http://doi.acm.org.ezproxy.lib.utexas.edu/10.1145/2535838.2535840
28 Apr 2015 — John — Roşu, Grigore; Şerbănuță, Traian Florin. An overview of the K semantic framework. The Journal of Logic and Algebraic Programming. 2010 Aug; 79(6): 397–434. Available from: http://www.sciencedirect.com.ezproxy.lib.utexas.edu/science/article/pii/S1567832610000160
05 May 2014 — Loc — Harris, Tim; Plesko, Mark; Shinnar, Avraham; Tarditi, David. Optimizing memory transactions. In Proceedings of the 2006 ACM SIGPLAN conference on Programming language design and implementation (PLDI '06). ACM; 2006. p. 14–25. http://doi.acm.org.ezproxy.lib.utexas.edu/10.1145/1133981.1133984
JIT
Dependent types
Safety in concurrent programs
Date — Lead by — Paper citation
09 Sep 2014 — — (Organizational meeting)
16 Sep 2014 — Arthur — Andreas Gal; Brendan Eich; Mike Shaver; David Anderson; David Mandelin; Mohammad R. Haghighat; Blake Kaplan; Graydon Hoare; Boris Zbarsky; Jason Orendorff; Jesse Ruderman; Edwin W. Smith; Rick Reitmaier; Michael Bebenita; Mason Chang; Michael Franz. 2009. Trace-based just-in-time type specialization for dynamic languages. In Proceedings of the 2009 ACM SIGPLAN conference on Programming language design and implementation (PLDI '09). ACM, 465–478. http://doi.acm.org.ezproxy.lib.utexas.edu/10.1145/1542476.1542528
23 Sep 2014 — Keshav — Nicolas Oury; Wouter Swierstra. 2008. The power of Pi. In Proceedings of the 13th ACM SIGPLAN international conference on Functional programming (ICFP '08). ACM, 39-50. http://doi.acm.org.ezproxy.lib.utexas.edu/10.1145/1411204.1411213
30 Sep 2014 — John — Mandana Vaziri; Frank Tip; Julian Dolby. 2006. Associating synchronization constraints with data in an object-oriented language. In Conference record of the 33rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages (POPL '06). ACM, 334–345. http://doi.acm.org.ezproxy.lib.utexas.edu/10.1145/1111037.1111067
07 Oct 2014 — Barry — Philip Wadler. 2003. Call-by-value is dual to call-by-name. In Proceedings of the eighth ACM SIGPLAN international conference on Functional programming (ICFP '03). ACM, New York, NY, USA, 189-201. http://doi.acm.org.ezproxy.lib.utexas.edu/10.1145/944705.944723
14 Oct 2014 — Arthur — Cormac Flanagan. 2006. Hybrid type checking. In Conference record of the 33rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages (POPL '06). ACM, 245–256. http://doi.acm.org.ezproxy.lib.utexas.edu/10.1145/1111037.1111059
21 Oct 2014 — Loc — William R. Cook; Walter Hill; Peter S. Canning. 1990. Inheritance is not subtyping. In Proceedings of the 17th ACM SIGPLAN-SIGACT symposium on Principles of programming languages (POPL '90). ACM, 125–135. http://doi.acm.org.ezproxy.lib.utexas.edu/10.1145/96709.96721
28 Oct 2014 — Loc — Koushik Sen. 2008. Race directed random testing of concurrent programs. In Proceedings of the 2008 ACM SIGPLAN conference on Programming language design and implementation (PLDI '08). ACM, 11–21. http://doi.acm.org.ezproxy.lib.utexas.edu/10.1145/1375581.1375584
18 Nov 2014 — Loc — Mayur Naik, Alex Aiken, and John Whaley. 2006. Effective static race detection for Java. In Proceedings of the 2006 ACM SIGPLAN conference on Programming language design and implementation (PLDI '06). ACM, 308–319. http://doi.acm.org.ezproxy.lib.utexas.edu/10.1145/1133981.1134018
25 Nov 2014 — Arthur — Tiark Rompf; Martin Odersky. 2010. Lightweight modular staging: A pragmatic approach to runtime code generation and compiled DSLs. In Proceedings of the Ninth International Conference on Generative Programming and Component Engineering (GPCE '10). ACM, 127–136. http://doi.acm.org.ezproxy.lib.utexas.edu/10.1145/1868294.1868314
02 Dec 2014 — John — Kohei Honda; Nobuko Yoshida; Marco Carbone. 2008. Multiparty asynchronous session types. In Proceedings of the 35th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages (POPL '08). ACM, 273–284. http://doi.acm.org.ezproxy.lib.utexas.edu/10.1145/1328438.1328472
Homotopy type theory
Session types
Compilation techniques including JIT
Date — Lead by — Paper citation
15 Apr 2014 — Keshav — Chapter one of: The Univalent Foundations Program, Institute for Advanced Study. 2013. Homotopy Type Theory: Univalent Foundations of Mathematics. Institute for Advanced Study, Princeton, NJ, USA. URL: http://homotopytypetheory.org/book/
06 May 2014 — Arthur — Tiarkv Rompf; Arvind K. Sujeeth; Kevin J. Brown; HyoukJoong Lee; Hassan Chafi; Kunle Olukotun. 2014. Surgical Precision JIT Compilers. To appear in PLDI 2014. Retrieved from http://lampwww.epfl.ch/~rompf/pldi2014.pdf
Impact of static typing
Progressive types
Set theory & type theory
Date — Lead by — Paper citation
10 Oct 2012 — Alex — Clemens Mayer; Stefan Hanenberg; Romain Robbes; Éric Tanter; Andreas Stefik. 2012. Static type systems (sometimes) have a positive impact on the usability of undocumented software: An empirical evaluation. To appear in Proc. OOPSLA 2012.
17 Oct 2012 — Ben — Joe Gibbs Politz; Hannah Quay-de la Vallee; Shriram Krishnamurthi. 2012. Progressive Types. To appear in Proc. SPLASH Onward! 2012.
14 Nov 2012 — John — James H. Morris, Jr.. 1973. Types are not sets. In Proceedings of the 1st annual ACM SIGACT-SIGPLAN symposium on Principles of programming languages (POPL '73). ACM, New York, NY, USA, 120-124. DOI=10.1145/512927.512938
also on 14 Nov — John C. Reynolds. 1974. Towards a theory of type structure. In Programming Symposium, Proceedings Colloque sur la Programmation, Bernard Robinet (Ed.). Springer-Verlag, London, UK, 408-423.
Functional synthesis
Template-driven synthesis
Sketching
Deductive synthesis
Concurrent program synthesis
Guided synthesis
Program repair
Verification
Verifier synthesis
Date — Lead by — Paper citation
05 Jul 2012 —
Roopsha — Roopsha Samanta. 2012. Towards algorithmic synthesis of synchronization for shared-memory concurrent programs.
Srinivas — Srinivas Nedunuri. 2012. Theory and Techniques for Synthesizing a Family of Graph Algorithms.
Practice talks for SYNT 2012 at CAV.
16 Jul 2012 — Zubair — Rishabh Singh; Armando Solar-Lezama. 2011. Synthesizing data structure manipulations from storyboards. In Proc. ESEC/FSE '11. ACM, 289-299.
27 Jul 2012 — Ben — Adam Chipala. Deductive synthesis in Coq using Certified Programming with Dependent Types. http://adam.chlipala.net/cpdt/
10 Aug 2012 — Srinivas — (A guided synthesis paper)
Kuperstein, M; Vechev, M; Yahav, E. Automatic inference of memory fences. In Proc. FMCAD 2010. IEEE, 111-119.
Kuncak, V; Mayer, M; Piskac, R; Suter, P. Complete functional synthesis. In Proc. PLDI 2010. ACM, 316-329.
Solar-Lezama, A; Jones C.; Bodik, R. Sketching concurrent data structures. In Proc. PLDI 2008. ACM, 136-148.
Solar-Lezama, A; Tancau, L; Bodik, R; et al. Combinatorial sketching for finite programs. In Proc. ASPLOS 2006. ACM, 404-415.
Srivastava, S; Gulwani, S; Foster, JS. From program verification to program synthesis. In Proc. POPL 2010. ACM, 313-326.
Srivastava, S; Gulwani, S; Foster, JS. Template-based Program Verification and Program Synthesis. In Journal on Software Tools for Technology Transfer.
Grebenshchikov, S; Lopes, NP, Popeea, C; Rybalchenko, A. Synthesizing software verifiers from proof rules. In Proc. PLDI 2012. ACM, 405-416.
21 Jun 2011
Formal Derivation of Concurrent Garbage Collectors. Pavlovic et. al. Mathematics of Program Construction 2010.
CoW: TBD.
14 Jun 2011
Path-based Inductive Synthesis for Program Inversion. Sriastava et al. PLDI 2011.
CoW: Key Lime Cupcakes and Banana Cupcakes with Peanut Butter Frosting.
07 Jun 2011
From Program Verification to Program Synthesis. Sriastava et al. POPL 2010.
CoW: Cashew Butterscotch Bars and Andrea's Homemade Chocolate Chip Cookies
31 May 2011
Data Representation Synthesis. Hawkins et al. PLDI 2011.
CoW: Blueberry and Cream Cookies
24 May 2011
Organizational Meeting. We'll kick things off with a broad discussion of current trends in synthesis and people's interests. We'll also choose papers for the rest of the summer, so bring suggestions! Dimensions in Program Synthesis. Sumit Gulwani. Principles and Practice of Declarative Programming. Good overview of the field, should help prime the pump for our discussion.
Cookie of the Week: Lemon Ricotta Cookies with Lemon Glaze
14 Sep 2010
Scrap your boilerplate with class: extensible generic functions Ralf Laemmel and Simon Peyton Jones, submitted to ICFP 2005. Amin Shali is presenting.
07 Sep 2010
Scrap Your Boilerplate: A Practical Approach to Generic Programming. Ralf Laemmel and Simon Peyton Jones, TLDI 2003. Ben D. is presenting.
Dependently Typed Languages and Their Applications
05 Oct 2010
The view from the left. Connor McBride and James McKinna. Journal of Functional Programming, Vol. 14. Published version Presented by Ben Delaware.
12 Oct 2010
Scrapping your Inefficient Engine: using Partial Evaluation to Improve Domain-Specific Language Implementation. Edwin Brady and Kevin Hammond. ICFP 2010. Published version Presented by Alex Loh.
26 Oct 2010
Rethinking Supercompilation Neil Mitchell, ICFP 2010. Carrying on our discussion of PE papers from ICFP this year. Presented by John Thywissen
02 Nov 2010
Supercompilation by Evaluation. Max Bolingbroke and Simon Peyton Jones. Presented by Ben D.
09 Nov 2010
The Power of Pi. Nicolas Oury and Wouter Swierstra, ICFP 2008. Presented by Reza M. Published version
16 Nov 2010
Amin Shali
23 Nov 2010
Reza M
07 Dec 2010
Srinivas
Potential papers for the coming semester:
The Gentle Art of Levitation. James Chapman, Pierre-Évariste Dagand, Conor McBride and Peter Morris. ICFP 2010.
Mint: Java Multi-stage Programming Using Weak Separability. Edwin Westbrook et. al. PLDI 2010.
Complete Functional Synthesis. V Kuncak, M. Mayer, R. Piskac, P. Suter. PLDI 2010.
Ur: Statically-Typed Metaprogramming with Type-Level Record Computation. Adam Chlipala. PLDI 2010.
A Simple Inductive Synthesis Methodology and its Applications. S Itzhaky et. al. SPLASH/OOPSLA 2010.
Type Classes as Objects and Implicits. BCS Oliveira et. al. SPLASH/OOPSLA 2010.
5/5/10
Towards unifying partial evaluation, deforestation, supercompilation, and GPC. M. Sørensen, R. Glück, N. D. Jones. ESOP '94.
4/23/10
Scalable component abstractions. Odersky, M. and Zenger, M. 2005. OOPSLA '05.
This paper touches on some of the same ideas as Derek Dreyer's talk, giving us an opportunity to revisit last Thursday's talk as well. There will be Milano cookies (they're distinctive).
4/09/10
Srinivas will be giving a practice talk for his upcoming presentation at the NASA Formal Methods Symposium .
4/02/10
We'll be continuing our discussion on coalgebras, focusing on Dana Schmidt's paper.
3/24/10
In a follow up to our paper on coalgebras, we'll be looking at coinduction and its uses as a proof technique. There are two readings for this week, plus an optional third paper:
In Types and Programming Languages, Chapter 21: Metatheory of Recursive Types up to 21.6. A good review of fixed points and their relation to induction and coinduction.
Trace-Based Abstract Interpretation of Operational Semantics by Dave Schmmidt, Chapters 3-5. Another example of coinduction featuring proofs about non-terminating programs.
Optional: Coinductive big-step operational semantics by Xavier Leroy. A more in-depth example of how coinduction can be used to reason about Big-Step Operational Semantics.
3/3/10
Threesomes, With and Without Blame. Jeremy G. Siek and Philip Wadler, POPL 2010. Bring your paper suggestions for the semester (again).
2/24/10
Pure subtype systems. DeLesley S. Hutchins, POPL 2010. Bring your paper suggestions for the semester.
12/09/09
Ben D.'s Coq Talk - Adaptation of Ben Pierce's Coq lecture notes + system walkthrough. Be sure to install Coq on your laptop to join in the fun!
12/02/09
Batch Discussion.
11/18/09
The Paradoxical Success of Aspect-Oriented Programming by Friedrich Steimann
10/28/09
No meeting. At OOPSLA
10/21/09
Foldl and foldr considered (slightly) harmful. Guy Steele 2009 Here is a video to go along with the paper
10/14/09
Meeting with Gérard Huet
9/30/09
NO Meeting!
9/23/09
Functional Programming with Bananas, Lenses, Envelopes and Barbed Wire. Erik Meijer, Maarten Fokkinga, and Ross Paterson, 1991.
9/16/09
On Understanding Data Abstraction, Revisited. William R. Cook, 2009.
Independently Extensible Solutions to the Expression Problem. Martin Odersky and Matthias Zenger, 2005.
5/27/09: Two papers on Coalgebra
A Tutorial on (Co)Algebras and (Co)Induction by Bart Jacobs, Jan Rutten
. http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.37.1418
Objects And Classes, Co-Algebraically by Bart Jacobs http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.54.7619
5/20/09: NO MEETING
5/13/09: Status meeting
5/6/09: Power of PI and Modeling discussion
4/29/09: Room Change ACES 2.404B
4/22/09: The Power of Pi
The Power of Pi. Nicolas Oury and Wouter Swierstra, 2008.
4/8/09: Policy-Based Authorization
Policy-Based Authorization William Cook
4/1/09: Abstract Interpretation (cut: and Application to Logic Programs)
Abstract Interpretation (cut: and Application to Logic Programs). Cousot & Cousot, 1992.
3/25/09: Status meeting: Pummel, DB/Batching, Orc, Synthesis
3/18/09: No meeting, spring break
3/11/09: Continue discussion and review derivation of sorting
Mechanizing the Development of Software - Doug Smith. NOTE THAT we will meet in the open conference area near my office for this week only.
3/04/09: Mechanizing the Development of Software
Mechanizing the Development of Software - Doug Smith, 1999
Feedback: I found the first meeting very educational. I wouldn't mind continuing discussion of the Smith paper, especially if we could focus on the practical issues of this approach:
which application domains it has trouble with
how to deal with changing requirements
how to generate efficient imperative implementations
how to debug faulty or incomplete specifications
how to interoperate with legacy systems
generally how practical it is for general-purpose programming
On Decidability of Nominal Subtyping with Variance. Andrew Kennedy and Benjamin Pierce, 2006.
Logical view of effects. Bob Harper and Sungwoo Park, 2004.
Coalgebras, Stone Duality, and Modal Logic. Kurz 2006