## Logic and Computer ScienceThe application of mathematical logic to computer science continues to be of major importance in the development of more advanced systems. In this book, a combination of survey chapters and applications work is presented--particularly concentrating on lamda-calculus, typed functional programming, and theorem provers |

### What people are saying - Write a review

We haven't found any reviews in the usual places.

### Contents

The basic system | 21 |

Recursive types | 36 |

Intersection types | 49 |

Copyright | |

25 other sections not shown

### Other editions - View all

Logic and Computer Science Piergiorgio Homer Steven Odifreddi,Anil Nerode,Richard A. Platek No preview available - 2014 |

### Common terms and phrases

abstraction application arithmetic axioms calculus of constructions candidates of reducibility closure Computer Science constants context Coppo Coquand corresponding data types defined Definition denote derivation domain ENOD equation equivalence example existential extended finite first-order first-order logic Girard sets given Harrop formulae higher-order logic Horn clauses Huet induction hypothesis inference rules infinite interpretation introduced intuitionistic intuitionistic logic Isabelle lambda terms Leivant Lemma maps Martin-L6f Math mathematics natural deduction natural numbers normal form notion Nuprl polymorphic lambda calculus predicate primitive programming languages proof theory Prop properties propositions prove quantifiers raw term recursion theory recursive functions recursive types reduction relation representation result saturated sets Section semantics sequent set of types set theory simple simply typed strong normalization strongly normalizable subset substitution syntactic tactic term of type Theorem type assignment type inference type theory type variables type-checks typing judgements uniform proof universal untyped lambda