Closure calculus is simpler than pure lambda-calculus as it does not mention free variables or index manipulation, variable renaming, implicit substitution, or any other meta-theory. Further, all programs, even recursive ones, can be expressed as normal forms. Third, there are reduction-preserving translations to calculi built from combinations of operators, in the style of combinatory logic. These improvements are achieved without sacrificing three fundamental properties of lambda-calculus, being a confluent rewriting system, supporting the Turing computable numerical functions, and supporting simple typing.
Method Rename has been a widely used refactoring operation that improves program
comprehension and maintenance. Descriptive method names that summarize
functionalities of source code can facilitate program comprehension. Much
research has been done to suggest method names through source code
summarization. However, unlike natural language, a code snippet consists of
basic blocks organized by complicated structures. In this work, we observe a
hierarchical structure --- tokens form basic blocks and basic blocks form a code
snippet. Based on this observation, we exploit a hierarchical attention network
to learn the representation of methods. Specifically, we apply two-level
attention mechanism to learn the importance of each token in a basic block and
that of a basic block in a method respectively. We evaluated our approach on 10
open source repositories and compared it against three state-of-the-art
approaches. The results on these open-source data show the superiority of our
hierarchical attention networks in terms of effectiveness.
Various methods have recently been proposed for temporal property verification of higher-order programs. In those methods, however, either temporal properties were limited to linear-time ones, or target programs were limited to finite-data programs. In this paper, we extend Kobayashi et al.'s recent method for verification of linear-time temporal properties based on HFLZ model checking, to deal with branching-time properties. We formalize branching-time property verification problems as an extension of HORS model checking called HORSZ model checking, present a sound and complete reduction to validity checking of (modal-free) HFLZ formulas, and prove its correctness. The correctness of the reduction subsumes the decidability of HORS model checking. The HFLZ formula obtained by the reduction from a HORSZ model checking problem can be considered a kind of verification condition for the orignal model checking problem. We also discuss interactive and automated methods for discharging the verification condition.
Regular expressions are used for a wide variety of purposes
from web-page input validation to log file crawling.
Very often, they are used not only to match strings, but
also to extract data from them.
Unfortunately, most regular expression engines
only return a list of the substrings captured by the regular
expression. The data has to be extracted from the
matched substrings to be validated and transformed manually into
a more structured format.
For richer classes of grammars like CFGs, such issues
can be solved using type-indexed combinators.
Most combinator libraries provide
a monadic API to track
the type returned by the parser through easy-to-use combinators.
This allows users to
transform the input into a custom data-structure and go through
complex validations as they describe their grammar.
In this paper, we present the Tyre library which provides
type-indexed combinators for regular languages.
Our combinators provide type-safe extraction
while delegating the task of substring matching to a preexisting
regular expression engine.
To do this, we use a two layer approach where the typed
layer sits on top of an untyped layer.
This technique is also amenable to several extensions, such as
routing, unparsing and static generation of the extraction code.
We also provide a syntax extension, which recovers
the familiar and compact syntax of regular expressions.
We implemented this technique in a very concise
manner and evaluated its usefulness on two practical examples.
There have been two major approaches to fully automated verification of higher-order functional programs:
higher-order model checking and refinement type inference.
The former approach is precise, but suffers from a bottleneck in the predicate discovery phase.
The latter approach is generally faster than the former,
thanks to the recent advances in constrained Horn clause (CHC) solving,
but is imprecise, in that it rejects some valid programs.
To take the best of the two approaches, we refine the higher-order model checking approach,
by employing CHC solving in the predicate discovery phase. We have
implemented the new approach
and confirmed that the new system can verify more programs than
those based on the previous two approaches.
Control flow obfuscation protects software from
being reverse-engineered by altering the control flow transfer without
without changing the software's run-time semantics.
We propose a new control flow obfuscation technique
by rewriting the source program in the continuation passing style (CPS).
The continuation is encoded through higher order
combinators and function pointers at the
target language level. As a result, the original control
flow graph is fragmented which makes any software tampering attempt through binary
static analysis hard. We implemented a prototype which performs
obfuscation on C source codes. The benchmark shows
that this approach is practical compared to existing techniques.
It is well known that the computational content of a termination proof
of a calculus is an interpreter that computes the result of an input
term.
Traditionally, such extraction has been tried for a calculus with
deterministic reduction rules, producing the result as a value, i.e.,
in weak head normal form where no redexes are reduced under lambda.
In this paper, we consider non-deterministic reduction rules where any
redexes can be reduced, even the ones under lambda, and extract a
partial evaluator, rather than an interpreter, that produces the
result in normal form.
We formalize a call-by-name, simply-typed, lambda calculus in the
Agda proof assistant and prove its termination using a logical
predicate.
We observe that the extracted program can be regarded as an online
partial evaluator and present future perspectives about how we can
extend the framework to a call-by-value calculus.
Futures and promises are a high-level concurrency construct to aid the user in writing scalable and correct asynchronous programs.
We introduce a simple core language based on which we can derive a rich set of future and promise features.
We discuss ways to implement the core features via shared-state concurrency
making either use of Software Transactional Memory,
an elementary lock-based primitive,
or an atomic compare-and-swap operation.
The approach has been fully implemented in Haskell and Scala.
For both languages, we provide empirical evidence of the effectiveness of our method.
We consider program transformations in the context of futures and promises
and observe potential problems in existing Scala-based libraries.
Many functional programs — state machines [Krishnamurthi 2006], top-down and bottom-up parsers [Hinze and Paterson 2003; Hutton and Meijer 1996], evaluators [Abelson et al. 1984], GUI initialization graphs [Syme 2006], &c. — are conveniently expressed as groups of mutually recursive bindings. One therefore expects program generators, such as those written in MetaOCaml, to be able to build programs with mutual recursion.
Unfortunately, currently MetaOCaml can only build recursive groups whose size is hard-coded in the generating program. The general case requires something other than quotation, and seemingly weakens static guarantees on the resulting code. We describe the challenges and propose a new language construct for assuredly generating binding groups of arbitrary size – illustrating with a collection of examples for mutual, n-ary, heterogeneous, value and polymorphic recursion.