scientific article; zbMATH DE number 3513750

zbMATH Open0328.02014MaRDI QIDQ4093416FDOQ4093416

Authors: W. W. Tait 

Publication date: 1975

Title of this publication is not available (Why is that?)

Mathematics Subject Classification ID

Intermediate logics (03B55) Higher-type and set recursion theory (03D65) Intuitionistic mathematics (03F55)

Cited In (21)

• Polymorphic rewriting conserves algebraic strong normalization
• A simple proof of second-order strong normalization with permutative conversions
• Algebraic types in PER models
• Typing and computational properties of lambda expressions
• Typing untyped \(\lambda\)-terms, or reducibility strikes again!
• Strong normalization from weak normalization in typed \(\lambda\)-calculi
• Strong normalization and typability with intersection types
• Termination of rewrite relations on \(\lambda\)-terms based on Girard's notion of reducibility
• A short and flexible proof of strong normalization for the calculus of constructions
• Constructive logics. I: A tutorial on proof systems and typed \(\lambda\)- calculi
• Typing termination in a higher-order concurrent imperative language
• The calculus of constructions
• Two extensions of System F with (co)iteration and primitive (co)recursion principles
• On the Values of Reducibility Candidates
• On strong normalization and type inference in the intersection type discipline
• Reducibility: a ubiquitous method in lambda calculus with intersection types
• On the versatility of open logical relations. Continuity, automatic differentiation, and a containment theorem
• Behavioural inverse limit \(\lambda\)-models
• Non-strictly positive fixed points for classical natural deduction
• Modular properties of algebraic type systems
• Proving properties of typed \(\lambda\)-terms using realizability, covers, and sheaves

This page was built for publication:

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4093416)