The 9th European Lisp Symposium is over!
This year's Highlights:
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.
Julia is a general purpose dynamic language, designed to make numerical computing fast and convenient. Many aspects of Julia should be quite familiar since they are "stolen" straight from Lisp: it’s expression-oriented, lexically scoped, has closures, coroutines, and macros that operate on code as data. But Julia departs from the Lisp tradition in other ways. Julia has syntax – lots of it. Macro invocations look different than function calls. Some dynamic behaviors are sacrificed to make programs easier to analyze (for both humans and compilers), especially where it allows simpler, more reliable program optimization.
Julia’s most distinctive feature is its emphasis on creating lightweight types and defining their behavior in terms of generic functions. While many Lisps support multiple dispatch as an opt-in feature, in Julia all function are generic by default. Even basic operators like `+` are generic, and primitive types like `Int` and `Float64` are defined in the standard library, and their behavior is specified via multiple dispatch. A combination of aggressive method specialization, inlining and data-flow-based type inference, allow these layers of abstraction and dispatch to be eliminated when it counts – Julia generally has performance comparable to static languages.
In the tradition of the great Lisp hackers, this talk will include lots of live coding in the REPL, with all the excitement, and possibility of failure entailed.
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)