From Contracts Towards Dependent Types: Proofs by Partial Evaluation

Abstract. The specification and resolution of non-trivial domain constraints has become a well-recognised measure for improving the stability of large software systems. In this paper we propose an approach based on partial evaluation which tries to prove such constraints statically as far as possible and inserts efficient dynamic checks otherwise.

• Type: Conference
• Year: 2007
• Where: IFL
• Authors: Stephan Herhut, Sven-Bodo Scholz, Robert Bernecky, Clemens Grelck, Kai Trojahner
• Keywords: Efficient Dynamic Checks, IFL 2007, Large Software Systems, Natural Language Processing, Non-trivial Domain Constraints