Programming in Martin-Löf's Type Theory: An Introduction

Bengt Nordström