BEGIN:VCALENDAR PRODID;X-RICAL-TZSOURCE=TZINFO:-//Calagator//EN CALSCALE:GREGORIAN X-WR-CALNAME:Calagator METHOD:PUBLISH VERSION:2.0 BEGIN:VTIMEZONE TZID;X-RICAL-TZSOURCE=TZINFO:America/Los_Angeles BEGIN:STANDARD DTSTART:20091101T020000 RDATE:20091101T020000 RDATE:20101107T020000 RDATE:20111106T020000 RDATE:20121104T020000 RDATE:20131103T020000 RDATE:20141102T020000 TZOFFSETFROM:-0700 TZOFFSETTO:-0800 TZNAME:PST END:STANDARD BEGIN:DAYLIGHT DTSTART:20100314T020000 RDATE:20100314T020000 RDATE:20110313T020000 RDATE:20120311T020000 RDATE:20130310T020000 RDATE:20140309T020000 RDATE:20150308T020000 TZOFFSETFROM:-0800 TZOFFSETTO:-0700 TZNAME:PDT END:DAYLIGHT END:VTIMEZONE BEGIN:VEVENT CREATED;VALUE=DATE-TIME:20100119T013639Z DTEND;TZID=America/Los_Angeles;VALUE=DATE-TIME:20100216T203000 DTSTART;TZID=America/Los_Angeles;VALUE=DATE-TIME:20100216T183000 DTSTAMP;VALUE=DATE-TIME:20100119T013639Z LAST-MODIFIED;VALUE=DATE-TIME:20100216T173554Z UID:http://calagator.org/events/1250458182 DESCRIPTION:This month's topic: An Argument for Semantics - Why Develope rs Should Give a Hoot about OWL \;\n \;\nIn the push to make use o f tagging and other forms user-driven information architectures\, develo pers have overlooked the value of adding semantics\, or contextual meani ng\, directly to the data that powers web sites and applications. The ad dition of Microformats to a Web site's markup can further the exchange o f semantic information such as contact information for people and events . For the most part\, however\, web sites and applications are still pop ulated by largely non-semantic prose organized in large blocks of HTML o r generated from the walled gardens of relational databases and data war ehouses. \;\n \;\nWhile everyone agrees that HTML isn't going away anytime soon\, several Web Standards have arisen over the last few year s to help application developers store\, serve\, and distribute informat ion with ever-increasing levels of semantics and meaning. The current pi nnacle of the Semantic Web Standards pyramid is OWL - the W3C's Web Onto logy Language. In this talk I will describe the roots and basics of OWL and how it can be used to power the next generation of smart\, data-enab led Web applications. \;\n \;\n---------- \;\n \;\nSpeaker: Brian Panulla \;\n \;\nBrian is a technology consultant and develo per for Dealerpeak - the Portland-based Web-enabled CRM for automotive d ealers. A recent transplant to Portland\, Brian formerly led grant-funde d R&\;D projects in the information sciences at Penn State University . He moved here primarily for the high quality and variety of beer. \ ;\n \;\n---------- \;\n \;\nPJUG meetings start with some time to eat and socialize (pizza and beverages are provided)\, followed by th e featured speaker\, then Q&\;A\, discussion\, sometimes a drawing to give away swag. :) \;\n \;\nThough we like knowing how many peopl e to expect\, you don't *have* to RSVP\, on Upcoming or otherwise. Go ah ead and just show up! \;\n \;\nMany people also go for a drink and further discussion following the meeting\, at a location determined ad hoc (lately\, the Market Street Pub at 10th and Market: http://mcmenamin s.com/index.php?loc=24 ). \;\n \;\nhttp://twitter.com/pjug \;\n http://pjug.org/ \;\n(join our mailing list\, linked from the website !)\n\nTags: java\, user group\, pjug\, oracle\, sun\, semantics\, owl\, bpanulla\, brian panulla\n\nImported from: http://calagator.org/events/1 250458182 URL:http://pjug.org/ SUMMARY:Portland Java User Group: An Argument for Semantics - Why Develop ers Should Give a Hoot about OWL LOCATION:Oracle (Downtown Campus): 1211 SW 5th Avenue\, Suite 800\, Room 8005\, Portland Oregon 97204 US SEQUENCE:7 END:VEVENT BEGIN:VEVENT CREATED;VALUE=DATE-TIME:20120103T181917Z DTEND;TZID=America/Los_Angeles;VALUE=DATE-TIME:20120110T113000 DTSTART;TZID=America/Los_Angeles;VALUE=DATE-TIME:20120110T103000 DTSTAMP;VALUE=DATE-TIME:20120103T181917Z LAST-MODIFIED;VALUE=DATE-TIME:20120103T181917Z UID:http://calagator.org/events/1250461795 DESCRIPTION:Presented by David Lazar \;\n \;\nFormal semantics is n otoriously hard. The K semantic framework (http://k-framework.org/) is a system that makes the task of formally defining programming languages e asy and practical. The primary goals of the K framework are modularity\, expressivity\, and executability. Adding a new language feature to a K definition does not require you to revisit and modify existing semantic rules. The K framework is able to concisely capture the semantics of non -determinism and concurrency. Each K definition automatically yields an interpreter for the language so that the definition can be tested for co rrectness. These features made it possible to develop a complete formal semantics of the C language in K. \;\nThe first half of the talk will be an overview of the K semantic framework. We'll discuss the merits of the framework using the K definition of a complex toy language as a gui ding example. The second half of the talk will focus on a work-in-progre ss formalization of Haskell 98 in K. We'll look at the challenges of for malizing Haskell and the applications of this work.\n\nTags: galois\, ha skell\, formal methods\, tech talk\, semantics\n\nImported from: http:// calagator.org/events/1250461795 URL:https://corp.galois.com/blog/2012/1/3/galois-tech-talk-1-of-3-next-we ek-formalizing-haskell-98-in.html SUMMARY:Galois Tech Talk (1 of 3 next week!): Formalizing Haskell 98 in t he K Semantic Framework LOCATION:Galois\, Inc: 421 SW 6th Ave. Suite 300\, Portland OR 97204 US SEQUENCE:1 END:VEVENT BEGIN:VEVENT CREATED;VALUE=DATE-TIME:20150608T184122Z DTEND;TZID=America/Los_Angeles;VALUE=DATE-TIME:20150618T110000 DTSTART;TZID=America/Los_Angeles;VALUE=DATE-TIME:20150618T100000 DTSTAMP;VALUE=DATE-TIME:20150608T184122Z LAST-MODIFIED;VALUE=DATE-TIME:20150608T184122Z UID:http://calagator.org/events/1250468603 DESCRIPTION:abstract: \;\n \;\nCH2O is the PhD project of Robbert K rebbers and has as its goal a formal version of the ISO standard of the C programming language. A problem with this is that the C standard is fu ndamentally inconsistent. \;\n \;\nThere are three versions of the CH2O semantics: a (small step) operational semantics\, an executable se mantics\, and an axiomatic semantics (a separation logic for C). The mos t important properties — soundness and completeness results\, subject re duction and progress\, correctness of the type checker — have all been p roved. All definitions and proofs have been fully formalized in Coq\, wi thout any axioms and on top of a non-trivial support library. \;\n 3\;\nThe CH2O project has two abstract C-like languages. A significant s ubset of C called “CH2O abstract C” is translated into a simplified lang uage called “CH2O core C”. This translation is written in Coq and implic itly gives a semantics to CH2O abstract C. The rest of the formalization is all about CH2O core C. \;\n \;\nThe executable CH2O semantics has been extracted to OCaml and combined with the CIL parser to a standa lone “interpreter”. This tool can be used to explore all behaviors of a program according to the C standard. Although the CH2O semantics does no t yet support I/O (nor the exit function)\, a small hack allows the CH2O interpreter to still explore programs that call printf. \;\n \;\n The CH2O semantics has been specifically designed to be compatible with the CompCert semantics for C. Significant differences between CompCert a nd CH2O are that the CH2O semantics has explicit typing judgments for ev erything\, and that CH2O applies to any ISO compliant compiler. \;\n& #13\;\nbio: \;\n \;\nI have a master degree in mathematics (my the sis was about conformal supergravity)\, and a PhD in computer science\, both from the University of Amsterdam. I also worked as a system adminis trator at the University of Utrecht. \;\n \;\nCurrently I’m an ass istant professor of computer science at the Radboud University Nijmegen. My research has been mainly about formalization of mathematics using in teractive theorem provers\, but recently I have been getting interested in practical program verification\, where interactive proof is used when automation doesn’t cut it. \;\n \;\nAt the moment I am an alterna te member of WG14\, and I won a price in the IOCCC twice. And my favorit e project is the CakeML/verified-HOL Light project. \;\n\n\nTags: Gal ois tech talk\, C\, theorem proving\, semantics\n\nImported from: http:/ /calagator.org/events/1250468603 URL:http://galois.com/blog/2015/06/tech-talk-ch2o-project-making-sense-c- standard/ SUMMARY:Galois tech talk: The CH2O project: making sense of the C standar d LOCATION:Galois\, Inc: 421 SW 6th Ave. Suite 300\, Portland OR 97204 US SEQUENCE:1 END:VEVENT END:VCALENDAR