APLAS 2024
Tue 22 - Fri 25 October 2024 Kyoto
Wed 23 Oct 2024 16:00 - 16:30 at Yamauchi Hall - Probabilistic and Declarative Programming Chair(s): Oleg Kiselyov

Functions containing arithmetic operations have often restrictions not expressible by standard type systems of programming languages. The division operation requires that the divisor is non-zero and the factorial function should not be applied to negative numbers. Such partial operations might lead to program crashes if they are applied to unintended arguments. Checking the arguments before each call is tedious and decreases the run-time efficiency. To avoid these disadvantages and support the safe use of partially defined operations, we present an approach to verify the correct use of operations at compile time. To simplify its use, our approach automatically infers non-fail conditions of operations from their definitions and checks whether these conditions are satisfied for all uses of the operations. Arithmetic conditions can be verified by SMT solvers, whereas conditions in operations defined on algebraic data types can be inferred and verified by appropriate type abstractions. Therefore, we present a hybrid method which is applicable to larger programs since only a few arithmetic non-fail conditions need to be checked by an external SMT solver. This approach is implemented for functional logic Curry programs so that it is also usable for purely functional or logic programs.

Wed 23 Oct

Displayed time zone: Osaka, Sapporo, Tokyo change

16:00 - 17:00
Probabilistic and Declarative ProgrammingResearch Papers at Yamauchi Hall
Chair(s): Oleg Kiselyov Tohoku University
16:00
30m
Talk
Hybrid Verification of Declarative Programs with Arithmetic Non-Fail Conditions
Research Papers
Michael Hanus Kiel University
16:30
30m
Talk
Explaining Explanations in Probabilistic Logic Programming
Research Papers
German Vidal Universitat Politecnica de Valencia