Deprecated: $wgMWOAuthSharedUserIDs=false is deprecated, set $wgMWOAuthSharedUserIDs=true, $wgMWOAuthSharedUserSource='local' instead [Called from MediaWiki\HookContainer\HookContainer::run in /var/www/html/w/includes/HookContainer/HookContainer.php at line 135] in /var/www/html/w/includes/Debug/MWDebug.php on line 372
scientific article - MaRDI portal

scientific article

From MaRDI portal

zbMath0311.02040MaRDI QIDQ4068706

Harvey M. Friedman

Publication date: 1975


Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.



Related Items

Fresh logic: Proof-theory and semantics for FM and nominal techniques, Word operation definable in the typed \(\lambda\)-calculus, Extended First-Order Logic, Kripke models and the (in)equational logic of the second-order \(\lambda\)-calculus, On the semantics of the universal quantifier, On Church's formal theory of functions and functionals. The \(\lambda\)- calculus: Connections to higher type recursion theory, proof theory, category theory, Polymorphic extensions of simple type structures. With an application to a bar recursive minimization, Embedding of a free cartesian-closed category into the category of sets, Parametricity of extensionally collapsed term models of polymorphism and their categorical properties, Typed homomorphic relations extended with subtypes, POPLMark reloaded: Mechanizing proofs by logical relations, A characterization of lambda definable tree operations, A Constructive Semantic Approach to Cut Elimination in Type Theories with Axioms, Finitely stratified polymorphism, Selective strictness and parametricity in structural operational semantics, inequationally, Characterizing complexity classes by higher type primitive recursive definitions, λ-definable functionals andβη conversion, The Typed Böhm Theorem, Constant time parallel computations in \(\lambda\)-calculus, What is the meaning of proofs?. A Fregean distinction in proof-theoretic semantics, Substitution structures, Intuitionistic propositional logic is polynomial-space complete, The typed lambda-calculus is not elementary recursive, A family of syntactic logical relations for the semantics of Haskell-like languages, Extensional models for polymorphism, Can LCF be topped! Flat lattice models of typed \(\lambda{}\)-calculus, Kripke Semantics for Martin-Löf’s Extensional Type Theory, Building continuous webbed models for system F, A semantics for nabla, Unnamed Item, Equality between functionals in the presence of coproducts, \(\lambda\)-definability of free algebras, Kripke-style models for typed lambda calculus, Set-theoretical and other elementary models of the \(\lambda\)-calculus