scientific article; zbMATH DE number 3513750
From MaRDI portal
Publication:4093416
zbMath0328.02014MaRDI QIDQ4093416
Publication date: 1975
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
Intuitionistic mathematics (03F55) Higher-type and set recursion theory (03D65) Intermediate logics (03B55)
Related Items
Algebraic types in PER models, On the Versatility of Open Logical Relations, Strong normalization from weak normalization in typed \(\lambda\)-calculi, The calculus of constructions, Strong normalization and typability with intersection types, A short and flexible proof of strong normalization for the calculus of constructions, Termination of rewrite relations on \(\lambda\)-terms based on Girard's notion of reducibility, On strong normalization and type inference in the intersection type discipline, Polymorphic rewriting conserves algebraic strong normalization, Behavioural inverse limit \(\lambda\)-models, Proving properties of typed \(\lambda\)-terms using realizability, covers, and sheaves, Modular properties of algebraic type systems, Constructive logics. I: A tutorial on proof systems and typed \(\lambda\)- calculi, Non-strictly positive fixed points for classical natural deduction, Typing termination in a higher-order concurrent imperative language, On the Values of Reducibility Candidates, Typing and computational properties of lambda expressions, Two extensions of system F with (co)iteration and primitive (co)recursion principles, Reducibility, A simple proof of second-order strong normalization with permutative conversions, Typing untyped \(\lambda\)-terms, or reducibility strikes again!