BibTeX

@inProceedings{johansson-etal-2014-hipster-216678,
	title        = {Hipster: Integrating theory exploration in a proof assistant},
	abstract     = {This paper describes Hipster, a system integrating theory exploration with the proof assistant Isabelle/HOL. Theory exploration is a technique for automatically discovering new interesting lemmas in a given theory development. Hipster can be used in two main modes. The first is exploratory mode, used for automatically generating basic lemmas about a given set of datatypes and functions in a new theory development. The second is proof mode, used in a particular proof attempt, trying to discover the missing lemmas which would allow the current goal to be proved. Hipster's proof mode complements and boosts existing proof automation techniques that rely on automatically selecting existing lemmas, by inventing new lemmas that need induction to be proved. We show example uses of both modes.},
	booktitle    = {Lecture Notes in Computer Science},
	author       = {Johansson, Moa and Rosén, Dan and Smallbone, Nicholas and Claessen, Koen},
	year         = {2014},
	volume       = {8543 },
	ISBN         = {978-3-319-08433-6},
	pages        = {108--122},
}

@misc{bernardy-etal-2014-compiling-195331,
	title        = {Compiling Linear Logic using Continuations},
	abstract     = {As System F is the logical foundation of functional programming, it has
long been expected that Classical Linear Logic (CLL) is the logical
foundation of concurrent programming.  In particular, thanks to an
involutive negation, its language of propositions correspond to protocols.
This means that CLL provides the principles to integrate concurrency into
functional programming languages.

Aiming towards this integration, we translate the concurrency features of
CLL into continuations, essentially via a negation-model of CLL into System
F.  Practically, the translation can be used to embed CLL programs into
functional languages such as Haskell. We explain the properties of the
interface between the two languages.  In particular, using an example, we
illustrate how the par (⅋) operator can solve practical functional
programming problems.
},
	author       = {Bernardy, Jean-Philippe and Rosén, Dan and Smallbone, Nicholas},
	year         = {2014},
}