1983/01/01 by Daniël Leivant · 1 citation
Computer Science · #Logic, programming, and type systems #Formal Methods in Verification #Parallel Computing and Optimization Techniques
paper · pdf · doi:10.1145/567067.567077
openalex publication_date 1983/01/01 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/31
The benefits of strong typing to disciplined programming, to compile-time error detection and to program verification are well known. Strong typing is especially natural for functional (applicative) languages, in which function application is the central construct, and type matching is therefore a principal program correctness check. In practice, however, assigning a type to each and every expression in a functional program can be prohibitively cumbersome. As expressions are compounded, the task of assigning a type to each expression and subexpression becomes practically impossible, even more so because the type-expressions themselves grow longer. It becomes imperative therefore to design friendly programming environments that permit the user type-free programming, but that generate fully typed programs in which the types of all expressions are inferred by the system from the program. For interactive functional programming environments of the kind implemented for the Edinburgh functional programming language ML, a type-inference system is an invaluable tool for on-line parse-time error detection and debugging.