Meeting notes: 2009-01-11 -- Agda theorem prover, Serialist.net, FP webapps, early-finish monad, HTTP Digest, etc

14 views
Skip to first unread message

Igal Koshevoy

unread,
Jan 15, 2010, 4:06:16 AM1/15/10
to pdxfunc
Please post corrections or additions.


VENUE

We met this month at the Roots Organic Brewery events room. This seemed like a better venue than NedSpace or the Lucky Lab. Unless someone has a better alternative, I propose that we have future meetings there. ADVANTAGES: Easy direct entry from the street, food and drinks service, lots of room, and many chairs and tables. DISADVANTAGES: Not free ($100/night, thanks to Bart Massey for splitting the cost with me), not in downtown or near rail transit which makes it harder to get to, room echoes badly, and we have to bring our own projector. During this meeting, there was a technical problem that caused their alarm to keep going off -- which isn't not normal, it was otherwise fairly quiet. Anyway, if we use this venue, the meetings will remain free -- you do not need to donate towards the room fee unless you feel like it.


PRESENTATIONS

"Agda proofs" by Julian Blake Kongslie
  • Agda overview: http://en.wikipedia.org/wiki/Agda_(theorem_prover)
  • Dependent types overview: http://en.wikipedia.org/wiki/Dependent_type
  • Agda is a functional programming language and theorem prover. It's stricter than languages like Haskell and lets you write more specific code. The programmer can describe their intent clearly enough that many logic errors can be prevented at compile-time. It provides dependent types, which are expression-like proofs that provide more sophisticated type checking than static types. It prevents you from writing incomplete programs and doesn't allow the use of general recursion because it's not possible to prove logic that doesn't terminate.

"Serialist: Lazy web-crawling in Haskell" by Jamey Sharp and Josh Triplett
  • The Serialist website (http://serialist.net/) provides a way to find, track and read serialized content (e.g., web comics). It's implemented entirely in Haskell and demonstrates functional web application development, crawling, scraping and distributed architecture. Serialist uses interesting graph algorithms to add and step through content lazily. Work on the site also produced useful, reusable Haskell modules: early-finish monad, HTTP Digest implementation, database layer, recursive monadic data structures, fast/lazy character converter, etc. Jamey and Josh will discuss these topics as well as their experiences analyzing and profiling their Haskell code to improve performance and reduce memory consumption.
  • Jamey Sharp's day job involves a computer test for attention deficit disorder, but his biggest projects have been the Portland State Aerospace Society, XCB, and Serialist. Twitter: @jamey_sharp. Projects: http://www.ohloh.net/accounts/jamey
  • Josh Triplett is a PhD student at Portland State University and a Free and Open Source Software hacker. He's involved in research on relativistic programming and advanced synchronization techniques for highly parallel systems. Josh builds and launches Linux-powered rockets with the Portland State Aerospace Society, and hacks on numerous other projects. Homepage with projects: http://joshtriplett.org/
  • See the fairly complete slides for of their talk: http://bit.ly/7Z4EDi
  • Code for the site, along with many reusable libraries, is available as open source: git clone git://serialist.net/git/serialist
  • If you'd like to help with the project, contact them: helpATserialistDOTnet.

-igal
Reply all
Reply to author
Forward
0 new messages