Æon is a programming language with refinement types that supports genetic programming for program synthesis.

 

import ../libraries/image;

is_image : (x:Integer) -> Boolean = uninterpreted;

type Image as {x:Integer | is_image(x) };

height : (x:Integer) -> Integer = uninterpreted;
width : (x:Integer) -> Integer = uninterpreted;

load_image : (name:String) -> {i:Image | height(i) == 75 } = native;

original : Image = loadImage("monalisa.jpg“, 75, 150);

evolveImage : {img : Image | width(original) == width(img) and
                             height(original) == height(img) and
                             polygons(img) < 500 and
                             @minimize (difference(original, img)} {
        ??hole
}

The Æon programming language  features

  • Restricted refinement types (a.k.a. Liquid Types)
  • Non-restricted refinement types, that have no restrictions and can be used to generate the fitness function.
  • Easy FFI layer that can interact with different languages (Python, Java, etc…)

 

Team

Alcides Fonseca

Project

Downloads

The current version of Aeon (3) is being developed at this repository. Please get in touch to get access.

Publications

  • Paulo Santos, Sara Silva, Alcides Fonseca, Refined Typed Genetic Programming as a user interface for Genetic Programming, Poster in GECCO 2020.
  • Alcides Fonseca, Paulo Santos, Sara Silva, The Usability Argument for Refined Typed Genetic Programming, Paper in PPSN 2020.

Paulo Santos was awarded the 2020 LASIGE Best Poster Award for Evolutionary Program Synthesis from Refined and Dependent type.