Author name cluster

Michael Hanus

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

11 papers

2 author rows

LOPSTR Conference 2025 Conference Paper

CurryInfo: Managing Analysis and Verification Information about Curry Packages

Michael Hanus

Abstract CurryInfo is a tool to manage information about program entities defined in modules of Curry packages. CurryInfo is designed as a generic and extensible system so that the kind of information ranges from syntactic (e. g. , comments, types, source code) to semantic aspects (e. g. , determinism, termination, total definition, non-failing). CurryInfo collects such information and provides various methods to access them. For instance, one can show this information in a REPL or IDE to help the programmer to select or use operations in an appropriate manner. Another application is to include this information in other tools to analyze or verify programs. Since CurryInfo manages a cache containing information about all Curry packages, this can speed up such tools on larger applications.

Details

LOPSTR Conference 2024 Conference Paper

Improving Logic Programs by Adding Functions

Michael Hanus

Abstract Logic programming is based on defining relations. Functions are often considered as syntactic sugar which can be transformed into predicates so that their logic is not used for computational purposes. In this paper, we present a method to use functions to improve the operational behavior of logic programs without loosing the flexibility of logic programming. For this purpose, predicates and goals are transformed into functions and nested expressions. By evaluating these functions in a demand-driven manner wherever possible and taking potential failures into account, we ensure that the execution of the transformed programs will never require more steps than the original programs but can decrease the number of steps—in the best case reducing infinite search spaces to finite ones. Thus, we obtain a systematic method to improve the operational behavior of logic programs without changing their semantics.

Details

LOPSTR Conference 2017 Conference Paper

Combining Static and Dynamic Contract Checking for Curry

Michael Hanus

Abstract Static type systems are usually not sufficient to express all requirements on function calls. Hence, contracts with pre- and postconditions can be used to express more complex constraints on operations. Contracts can be checked at run time to ensure that operations are only invoked with reasonable arguments and return intended results. Although such dynamic contract checking provides more reliable program execution, it requires execution time and could lead to program crashes that might be detected with more advanced methods at compile time. To improve this situation for declarative languages, we present an approach to combine static and dynamic contract checking for the functional logic language Curry. Based on a formal model of contract checking for functional logic programming, we propose an automatic method to verify contracts at compile time. If a contract is successfully verified, dynamic checking of it can be omitted. This method decreases execution time without degrading reliable program execution. In the best case, when all contracts are statically verified, it provides trust in the software since crashes due to contract violations cannot occur during program execution.

Details

LOPSTR Conference 2016 Conference Paper

CurryCheck: Checking Properties of Curry Programs

Michael Hanus

Abstract We present CurryCheck, a tool to automate the testing of programs written in the functional logic programming language Curry. CurryCheck executes unit tests as well as property tests which are parameterized over one or more arguments. CurryCheck tests properties by systematically enumerating test cases so that, for smaller finite domains, CurryCheck can actually prove properties. Unit tests and properties can be defined in a Curry module without being exported. Thus, they are also useful to document the intended semantics of the source code. Furthermore, CurryCheck also supports the automated checking of specifications and contracts occurring in source programs. Hence, CurryCheck is a useful tool that contributes to the property- and specification-based development of reliable and well tested declarative programs.

Details

LOPSTR Conference 2015 Conference Paper

From Boolean Equalities to Constraints

Sergio Antoy
Michael Hanus

Abstract Although functional as well as logic languages use equality to discriminate between logically different cases, the operational meaning of equality is different in such languages. Functional languages reduce equational expressions to their Boolean values, True or False, logic languages use unification to check the validity only and fail otherwise. Consequently, the language Curry, which amalgamates functional and logic programming features, offers two kinds of equational expressions so that the programmer has to distinguish between these uses. We show that this distinction can be avoided by providing an analysis and transformation method that automatically selects the appropriate operation. Without this distinction in source programs, the language design can be simplified and the execution of programs can be optimized. As a consequence, we show that one kind of equational expressions is sufficient and unification is nothing else than an optimization of Boolean equality.

Details

LOPSTR Conference 2005 Conference Paper

Declarative Programming with Function Patterns

Sergio Antoy
Michael Hanus

Abstract We propose an extension of functional logic languages that allows the definition of operations with patterns containing other defined operation symbols. Such “function patterns” have many advantages over traditional constructor patterns. They allow a direct representation of specifications as declarative programs, provide better abstractions of patterns as first-class objects, and support the high-level programming of queries and transformation of complex structures. Moreover, they avoid known problems that occur in traditional programs using strict equality. We define their semantics via a transformation into standard functional logic programs. Since this transformation might introduce an infinite number of rules, we suggest an implementation that can be easily integrated with existing functional logic programming systems.

Details

LOPSTR Conference 2004 Conference Paper

Run-Time Profiling of Functional Logic Programs

Bernd Braßel
Michael Hanus
Frank Huch
Josep Silva
Germán Vidal

Abstract In this work, we introduce a profiling scheme for modern functional logic languages covering notions like laziness, sharing, and non-determinism. Firstly, we instrument a natural (big-step) semantics in order to associate a symbolic cost to each basic operation (e. g. , variable updates, function unfoldings, case evaluations). While this cost semantics provides a formal basis to analyze the cost of a computation, the implementation of a cost-augmented interpreter based on it would introduce a huge overhead. Therefore, we also introduce a sound transformation that instruments a program such that its execution—under the standard semantics—yields not only the corresponding results but also the associated costs. Finally, we describe a prototype implementation of a profiler based on the developments in this paper.

Details

LPAR Conference 2000 Conference Paper

Using an Abstract Representation to Specialize Functional Logic Programs

Elvira Albert
Michael Hanus
Germán Vidal

Abstract This paper introduces a novel approach for the specialization of functional logic languages. We consider a maximally simplified abstract representation of programs (which still contains all the necessary information) and define a non-standard semantics for these programs. Both things mixed together allow us to design a simple and concise partial evaluation method for modern functional logic languages, avoiding several limitations of previous approaches. Moreover, since these languages can be automatically translated into the abstract representation, our technique is widely applicable. In order to assess the practicality of our approach, we have developed a partial evaluation tool for the multi-paradigm language Curry. The partial evaluator is written in Curry itself and has been tested on an extensive benchmark suite (even a meta-interpreter). To the best of our knowledge, this is the first purely declarative partial evaluator for a functional logic language.

Details

LPAR Conference 1999 Conference Paper

A Partial Evaluation Framework for Curry Programs

Elvira Albert
María Alpuente
Michael Hanus
Germán Vidal

Abstract In this work, we develop a partial evaluation technique for residuating functional logic programs, which generalize the concurrent computation models for logic programs with delays to functional logic programs. We show how to lift the nondeterministic choices from run time to specialization time. We ascertain the conditions under which the original and the transformed program have the same answer expressions for the considered class of queries as well as the same floundering behavior. All these results are relevant for program optimization in Curry, a functional logic language which is intended to become a standard in this area. Preliminary empirical evaluation of the specialized Curry programs demonstrates that our technique also works well in practice and leads to substantial performance improvements. To our knowledge, this work is the first attempt to formally define and prove correct a general scheme for the partial evaluation of functional logic programs with delays.

Details

LOPSTR Conference 1996 Conference Paper

Efficient Translation of Lazy Functional Logic Programs into Prolog

Michael Hanus

Abstract In this paper, we present a high-level implementation of lazy functional logic programs by transforming them into Prolog programs. The transformation is controlled by generalized definitional trees which specify the narrowing strategy to be implemented. Since we consider a sophisticated narrowing strategy, a direct mapping of functions into predicates is not possible. Therefore, we present new techniques to reduce the interpretational overhead of the generated Prolog code. This leads to a portable and efficient implementation of functional logic programs.

Details

TCS Journal 1991 Journal Article

Horn clause programs with polymorphic types: semantics and resolution

Michael Hanus

This paper presents a Horn clause logic where functions and predicates are declared with polymorphic types. Types are parameterized with type variables. This leads to an ML-like polymorphic type system. A type declaration of a function or predicate restricts the possible use of this function or predicate so that only certain terms are allowed to be arguments for this function or predicate. The semantic models for polymorphic Horn clause programs are defined and a resolution method for this kind of logic programs is given. It will be shown that several optimizations in the resolution method are possible for specific kinds of programs. Moreover, it is shown that higher-order programming techniques can be applied in our framework.

Details DOI