BEGIN:VCALENDAR
PRODID:-//CALENDARSERVER.ORG//NONSGML Version 1//EN
VERSION:2.0
BEGIN:VEVENT
ATTENDEE;CN=Emilio Jesús Gallego Arias;CUTYPE=INDIVIDUAL;EMAIL=no-reply@;ROLE=CHAIR;SCHEDULE-STATUS=1.1:mailto:no-reply@
ATTENDEE;CN=J B;CUTYPE=INDIVIDUAL;EMAIL=bart@magnetophon.nl;PARTSTAT=ACCEPTED;X-CALENDARSERVER-DTSTAMP=20150408T100340Z:/aMTcyOTE2NzEyNDE3MjkxNjz_AXXILdoPPXpYBxyJXr-2fWH5lTWHL2FCVtmRbBA2/principa
 l/
CATEGORIES:Paper Presentation
DESCRIPTION:We address the question of what software verification can do for the audio 
 community by showcasing some preliminary design ideas and tools for a new f
 ramework dedicated to the formal reasoning about Faust programs. We use as 
 a foundation one of the strongest current proof assistants\, namely Coq com
 bined with Ssreflect. We illustrate the practical import of our approach vi
 a a use case\, namely the proof that the implementation of a simple low-pas
 s filter written in the Faust audio programming language indeed meets one o
 f its specification properties.\n\nThe paper thus serves three purposes: (1
 ) to provide a gentle introduction to the use of formal tools to the audio 
 community\, (2) to put forward programming and formal reasoning paradigms w
 e think are well suited to the audio domain and (3) to illustrate this appr
 oach on a simple yet practical audio signal processing example\, a low-pass
  filter.
DTEND:20150411T141500Z
DTSTAMP:20150408T100324Z
DTSTART:20150411T133000Z
LAST-MODIFIED:20150408T100315Z
LOCATION:Main venue (P1)
ORGANIZER;CN=J B;EMAIL=bart@magnetophon.nl:/aMTcyOTE2NzEyNDE3MjkxNjz_AXXILdoPPXpYBxyJXr-2fWH5lTWHL2FCVtmRbBA2/principa
 l/
SEQUENCE:0
SUMMARY:LAC2015 - A Taste of Sound Reasoning
UID:lac2015-19@
END:VEVENT
END:VCALENDAR
