Programming Languages
We describe an integration of program synthesis into Uclid5, a formal modelling and verification tool. To the best of our knowledge, the new version of Uclid5 is the only tool that supports program synthesis with bounded model checking,…
In reversible computing, the management of space is subject to two broad classes of constraints. First, as with general-purpose computation, every allocation must be paired with a matching de-allocation. Second, space can only be safely…
BISM (Bytecode-Level Instrumentation for Software Monitoring) is a lightweight bytecode instrumentation tool that features an expressive high-level control-flow-aware instrumentation language. The language follows the aspect-oriented…
We study the fundamental efficiency of delimited control. Specifically, we show that effect handlers enable an asymptotic improvement in runtime complexity for a certain class of functions. We consider the generic count problem using a pure…
Decidability and synthesis of inductive invariants ranging in a given domain play an important role in many software and hardware verification systems. We consider here inductive invariants belonging to an abstract domain $A$ as defined in…
We present a system called Smyth for program sketching in a typed functional language whereby the concrete evaluation of ordinary assertions gives rise to input-output examples, which are then used to guide the search to complete the holes.…
We present an experimental system strongly inspired by miniKanren, implemented on top of the tactics mechanism of the HOL~Light theorem prover. Our tool is at the same time a mechanism for enabling the logic programming style for reasoning…
This paper presents a verification framework based on a new class of predicate Constraint Satisfaction Problems called pCSP where constraints are represented as clauses modulo first-order theories over function variables and predicate…
Term rewriting systems have a simple syntax and semantics and facilitate proofs of correctness. However, they are not as popular in industry or academia as imperative languages. We define a term rewriting based abstract programming language…
A recursive descent parser is built from a set of mutually-recursive functions, where each function directly implements one of the nonterminals of a grammar. A packrat parser uses memoization to reduce the time complexity for recursive…
This paper attempts to connects the evolution of computer languages with the evolution of life, where the later has been dictated by \emph{theory of evolution of species}, and tries to give supportive evidence that the new languages are…
We present a novel concept of universal text preprocessing and text-embedded programming (PTEP). Preprocessing and text-embedded programming has been widely used in programming languages and frameworks in a fragmented and mutually isolated…
Syntax errors are generally easy to fix for humans, but not for parsers in general nor LR parsers in particular. Traditional 'panic mode' error recovery, though easy to implement and applicable to any grammar, often leads to a cascading…
While the use of formal verification techniques is well established in the development of mission-critical software, it is still rare in the production of most other kinds of software. We share our experience that a formal verification tool…
This article presents liquid resource types, a technique for automatically verifying the resource consumption of functional programs. Existing resource analysis techniques trade automation for flexibility -- automated techniques are…
Automated techniques for rigorous floating-point round-off error analysis are important in areas including formal verification of correctness and precision tuning. Existing tools and techniques, while providing tight bounds, fail to analyze…
OCaml is an industrial-strength, multi-paradigm programming language, widely used in industry and academia. OCaml is also one of the few modern managed system programming languages to lack support for shared memory parallel programming.…
Since composed grammars are often ambiguous, grammar composition requires a mechanism for dealing with ambiguity: either ruling it out by using delimiters (which are awkward to work with), or by using disambiguation operators to filter a…
Ability to use definitions occurring in the code directly in equational reasoning is one of the key strengths of functional programming. This is impossible in the case of Haskell type class methods unless a particular instance type is…
We present Lifty, a domain-specific language for data-centric applications that manipulate sensitive data. A Lifty programmer annotates the sources of sensitive data with declarative security policies, and the language statically and…