Programming language built with subtyping (lattice typing) and categorical duality in mind. The core of the language is a term language for sequent calculus (rather than natural deduction as is typical for functional languages).