Welcome to the 9th European Lisp Symposium!
The purpose of the European Lisp Symposium is to provide a forum for the discussion and dissemination of all aspects of design, implementationand application of any of the Lisp and Lisp-inspired dialects, including Common Lisp, Scheme, Emacs Lisp, AutoLisp, ISLISP, Dylan, Clojure, ACL2, ECMAScript, Racket, SKILL, Hop and so on. We encourage everyone interested in Lisp to participate.
We'll be updating this website's contents on a regular basis. Stay tuned!
This year's Highlights:
This talk aims to present some aspects of the Coq proof assistant, mainly the possibility of verifying and/or synthesizing correct programs.
The talk will start with an introduction to the main features of Coq, both as a statically typed functional programming language and as a proof assistant, i.e. a tool for helping its user to prove theorems, including - but not limited to - correctness statements about his/her programs.
In the second part of the talk, we propose to use the efficient computa- tion of powers of the form xn as a pretext for presenting various techniques for obtaining certified programs within the Coq system, with various levels of automaticity. Besides "classical" proof methods, we will present briefly some approaches and compare them with respect to their ability to efficiently return correctness proofs.
- Proof by reflection,
- The "refinement for free" approach,
- Composition of certified components (correctness by construction)
The power of Common Lisp for Functional_Programming is well known, the key tool being the notion of "lexical closure", allowing the programmer to write programs which, during execution, dynamically generate functional objects of arbitrary complexity. Using this technology, new algorithms in Algebraic Topology have been discovered, implemented in Common Lisp and used, producing homology and homotopy groups so far unreachable. An algorithm is viewed as "tractable" if its theoretical complexity is not worse than polynomial. The study of this complexity for the aforementioned of Algebraic Topology algorithms requires a lucid knowledge of the concrete implementation of these lexical closures. This talk is devoted to a report about a result of polynomial complexity so obtained. The scope of the method is general and in particular no knowledge in Algebraic Topology is expected from the audience.
Want to know more about the European Lisp Symposium? Use the top buttons to navigate within this website, or press the Register button on your right to let us know you're coming!