2008/02/01 by Tim Sheard, Emir Pasalic · 1 citation
Computer Science · Mathematics · #Logic, programming, and type systems #Logic, Reasoning, and Knowledge #Formal Methods in Verification #Mega- #Programming language #Computer science #Functional logic programming #ENCODE #Data type #Answer set programming #Logic programming #First-generation programming language #Programming domain #Programming paradigm #Inductive programming #Type (biology) #Set (abstract data type) #Point (geometry) #Theoretical computer science #Mathematics
paper · pdf · doi:10.1016/j.entcs.2007.11.012
openalex publication_date 2008/02/01 · openalex created_date 2025/10/10 · openalex updated_date 2026/08/02
We report our experience with exploring a new point in the design space for formal reasoning systems: the development of the programming language Ωmega. Ωmega is intended as both a practical programming language and a logic. The main goal of Ωmega is to allow programmers to describe and reason about semantic properties of programs from within the programming language itself, mainly by using a powerful type system. We illustrate the main features of Ωmega by developing an interesting meta-programming example. First, we show how to encode a set of well-typed simply typed λ-calculus terms as an Ωmega data-type. Then, we show how to implement a substitution operation on these terms that is guaranteed by the Ωmega type system to preserve their well-typedness.