2012 · 47 citations · 32 references
ComputingComputer ScienceAlgorithmsProgramming LanguagesSyntaxAbstract Syntax TreesConstraint ProgrammingConstraint SolvingFunctional ProgrammingSpecification LanguagesType SystemsAlgebraic Data TypesAutomated Reasoning With ConstraintsConstraint-based ProgrammingDeclarative SemanticsFirst-class FunctionsSemantics Of ConstraintsType ConstraintsType-level Programming
We present an extension of Scala that supports constraint programming over bounded and unbounded domains. The resulting language, Kaplan, provides the benefits of constraint programming while preserving the existing features of Scala. Kaplan integrates constraint and imperative programming by using constraints as an advanced control structure; the developers use the monadic 'for' construct to iterate over the solutions of constraints or branch on the existence of a solution. The constructs we introduce have simple semantics that can be understood as explicit enumeration of values, but are implemented more efficiently using symbolic reasoning. Kaplan programs can manipulate constraints at run-time, with the combined benefits of type-safe syntax trees and first-class functions. The language of constraints is a functional subset of Scala, supporting arbitrary recursive function definitions over algebraic data types, sets, maps, and integers.
32
Joxan Jaffar, J.-L. Lassez · 1987 · 1.6K citations
On the synthesis of a reactive module
Amir Pnueli, Roni Rosner · 1989 · 1.4K citations · Full text
Daniel Jackson · ACM Transactions on Software Engineering and Methodology · 2002 · 1.2K citations
Simplify: a theorem prover for program checking
David Detlefs, Greg Nelson, James B. Saxe · Journal of the ACM · 2005 · 781 citations