Decidable Logic in the Design of Functional Languages

In this paper we present a call-by-value PCF that is a variant of typed lambda calculus with a decidable first order logic. The main motivation of this new call-by-value language is to verify the correctness and reliability of using decidable conditionals in the design of practical call-by-value functional languages. And another application of this new language is that it can be an intermediate language to compare expressiveness between functional languages after language design. We show that the new language has the least expressiveness as the original call-by-value PCF. The decidability of theoremhood in the new language can introduce dependent types to functional languages. A fully abstract encoding is given from original call-by-value PCF into the new language with respect to Abramsky's extended applicative bisimulation.