Lambda the Ultimate

Haskell-Like S-Expression-Based Language
Designed for an IDE

(has to have my current absolute super favourite first sentence ever.)

Abstract

The state of the programmers’ toolbox is abysmal. Although substantial effort is put into the
development of powerful integrated development environments (IDEs), their features often lack
capabilities desired by programmers and target primarily classical object oriented languages.
This report documents the results of designing a modern programming language with its IDE in
mind. We introduce a new statically typed functional language with strong metaprogramming
capabilities, targeting JavaScript, the most popular runtime of today; and its accompanying
browser-based IDE. We demonstrate the advantages resulting from designing both the language
and its IDE at the same time and evaluate the resulting environment by employing it to solve a
variety of nontrivial programming tasks. Our results demonstrate that programmers can greatly
benefit from the combined application of modern approaches to programming tools.

Typer: ML boosted with type theory and Scheme

Abstract
We present the language Typer which is a programming language in the ML family. Its
name is an homage to Scheme(r) with which it shares the design of a minimal core language
combined with powerful metaprogramming facilities, pushing as much functionality as
possible into libraries. Contrary to Scheme, its syntax includes traditional infix notation,
and its core language is very much statically typed. More specifically the core language is a
variant of the implicit calculus of constructions (ICC). We present the main elements of the
language, including its Lisp-style syntactic structure, its elaboration phase which combines
macro-expansion and Hindley-Milner type inference, its treatment of implicit arguments,
and its novel approach to impredicativity.

I am looking for a dependent research proof system language implemented in C++.