Talk's page https://scala.io/talks/logicmetapro...

Description:
Since the beginning of the 21st century, the functional programming paradigm, whose root ideas are now almost 100 years old, has finally trickled down to the rest of the community, bringing more safety and clarity to the more mainstream languages: several languages adopted the idiom of lambda functions, the Java community gave birth to Scala, Clojure, and Kotlin, that all include a substantial amount of functional features; most modern languages embrace immutability by default and feature a form of algebraic data types as well as lazy and/or stateless data structures; etc. In more confidential contexts, the logic programming paradigm, although more obscure, managed to remain stable in a niche of specific use cases: inference and unification problems, rulebased reasoning, combinatorics, constraint programming, operational research, etc.

In this talk, we will explore one of the areas where both of these unique yet powerful tools converge: using a logic programming language as a metalanguage for a functional programming language. First, we will present its use for implementing a typechecker, then for proof transfer in the context of dependentlytyped functional languages.


Enzo CRANCE
PhD Student
INRIA

PhD in Computer Science @ Inria Metaprogramming for Coq, formal proof automation Functional programming enjoyer

  / cranceltik  
  / enzocrance099628b9  



Scala.IO: https://scala.io
Director: Yann BRESSON
Camera Operator: Margot MOYON
Technical Support: Smartmedias www.smartmedias.fr