tag:calagator.org,2005:/events/searchCalagator: Events tagged with: coq2018-07-12T10:17:42-07:00tag:calagator.org,2005:Calagator::Event/12504608252011-07-14T13:02:47-07:002011-07-14T13:02:47-07:00Galois tech talk: Combining Denotational and Operational Semantics for Scalable Proof DevelopmentTuesday, July 19, 2011 from 10:30-11:30am at Galois, Inchttp://calagator.org/events/12504608252011-07-19T10:30:00-07:002011-07-19T11:30:00-07:00<div class="vevent">
<h1 class="summary">Galois tech talk: Combining Denotational and Operational Semantics for Scalable Proof Development</h1>
<div class='date'><time class="dtstart dt-start" title="2011-07-19T10:30:00" datetime="2011-07-19T10:30:00">Tuesday, July 19, 2011 from 10:30</time>–<time class="dtend dt-end" title="2011-07-19T11:30:00" datetime="2011-07-19T11:30:00">11:30am</time></div>
<div class="location vcard">
<a href='/venues/202390439' class='url'>
<span class='fn org'>Galois, Inc</span>
</a>
<div class="adr">
<div class="street-address">421 SW 6th Ave. Suite 300</div>
<span class="locality">Portland</span>
, <span class="region">OR</span>
<span class="postal-code">97204</span>
<div class='country-name'>US<div>
(<a href='https://maps.google.com/maps?q=421%20SW%206th%20Ave.%20Suite%20300,%20Portland%20OR%2097204%20US'>map</a>)
</div>
</div>
<div class="description">
<p>Presented by Adam Foltzer.</p>
<p>Interpreters offer a convenient and intuitive way for programmers to reason about language behavior through denotational semantics. However in a setting like Coq, where all recursive functions must provably terminate, it is impossible to write interpreters for non-terminating languages. The standard alternative is to inductively define operational semantics, but this can yield proofs that are difficult to automate, particularly in the presence of changing language features.</p>
<p>This talk presents a combined approach, where an interpreter is used in combination with operational semantics to prove type preservation of a small functional language. To demonstrate the scalability of the Coq development, let expressions and a pair types will be added and preservation will be proved again with only one extra line of proof script.</p>
<p>This technique and development are adapted from Greg Morrisett's lectures at the 2011 Oregon Programming Languages Summer School, and are available at his web site.</p>
</div>
<h3>Links</h3>
<ul>
<li><a class="url" href="http://corp.galois.com/blog/2011/7/14/tech-talk-combining-denotational-and-operational-semantics-f.html">Website</a></li>
</ul>
<div class="tags">
<h3>Tags</h3>
<p><a class="p-category" href="/events/tag/coq">coq</a>, <a class="p-category" href="/events/tag/galois">galois</a>, <a class="p-category" href="/events/tag/tech talk">tech talk</a>, <a class="p-category" href="/events/tag/theorem proving">theorem proving</a></p>
</div>
<div class='single_view_right'>
<a href='http://calagator.org/events/1250460825.ics'>Download to iCal</a>
<div id='edit_link'>
<p>You can <a href="http://calagator.org/events/1250460825/edit">edit this event</a>.</p>
</div>
<div id='metadata'>
This item was added directly to Calagator <br /><strong>Thursday, July 14, 2011 at 1:02pm</strong>.
</div>
</div>
</div>
45.5204 -122.6779tag:calagator.org,2005:Calagator::Event/12504739942018-07-12T10:17:42-07:002018-07-12T10:17:42-07:00Galois Tech Talk: Vellvm -- Verifying the LLVMFriday, July 13, 2018 from 11am-noon at Galois Inchttp://calagator.org/events/12504739942018-07-13T11:00:00-07:002018-07-13T12:00:00-07:00<div class="vevent">
<h1 class="summary">Galois Tech Talk: Vellvm -- Verifying the LLVM</h1>
<div class='date'><time class="dtstart dt-start" title="2018-07-13T11:00:00" datetime="2018-07-13T11:00:00">Friday, July 13, 2018 from 11am</time>–<time class="dtend dt-end" title="2018-07-13T12:00:00" datetime="2018-07-13T12:00:00">noon</time></div>
<div class="location vcard">
<a href='/venues/202394717' class='url'>
<span class='fn org'>Galois Inc</span>
</a>
<div class="adr">
<div class="street-address">421 Sw 6th Ave Ste 300</div>
<span class="locality">Portland</span>
, <span class="region">OR</span>
<span class="postal-code">97204</span>
<div class='country-name'>US<div>
(<a href='https://maps.google.com/maps?q=421%20Sw%206th%20Ave%20Ste%20300,%20Portland%20OR%2097204%20US'>map</a>)
</div>
</div>
<div class="description">
<p>Abstract:
In this talk, I’ll give a high-level overview of Penn’s Vellvm (Verified LLVM) project, which aims to build formal semantics in Coq for the LLVM IR. I’ll sketch some of our past results, in which we verified memory safety transformations and a variant of LLVM’s mem2reg optimization, focusing on the structure of the proof techniques. Along the way, I’ll highlight some of the challenges of reasoning about LLVM code (many of which are still open issues). I’ll wrap up with a status report about our ongoing efforts to re-engineer Vellvm as part of the DeepSpec NSF Expeditions project.</p>
<p>No experience with LLVM or Coq will be assumed.</p>
<p>Bio:
I study programming languages and computer security. I have wide-ranging interests, and some of my most recent work touches on: Coq verification of LLVM program transformations and randomized algorithms, type-directed program synthesis, linear types and GUI programming. I have also spent a lot of time thinking about language-based enforcement of information-flow policies, low-level code memory safety, understanding dynamic security policies, and authorization logic. I am also interested in secure concurrent and distributed computing, functional programming languages, type theory, linear and modal logics, theorem proving and mechanized metatheory.</p>
</div>
<h3>Links</h3>
<ul>
<li><a class="url" href="https://galois.com/blog/2018/07/vellvm-verifying-the-llvm/">Website</a></li>
</ul>
<div class="tags">
<h3>Tags</h3>
<p><a class="p-category" href="/events/tag/computer science">computer science</a>, <a class="p-category" href="/events/tag/coq">coq</a>, <a class="p-category" href="/events/tag/formal semantics">formal semantics</a>, <a class="p-category" href="/events/tag/llvm">llvm</a>, <a class="p-category" href="/events/tag/security">security</a>, <a class="p-category" href="/events/tag/verification">verification</a></p>
</div>
<div class='single_view_right'>
<a href='http://calagator.org/events/1250473994.ics'>Download to iCal</a>
<div id='edit_link'>
<p>You can <a href="http://calagator.org/events/1250473994/edit">edit this event</a>.</p>
</div>
<div id='metadata'>
This item was added directly to Calagator <br /><strong>Thursday, July 12, 2018 at 10:17am</strong>.
</div>
</div>
</div>
45.5208 -122.6779