Publication:5625124
From MaRDI portal
zbMath0221.02013MaRDI QIDQ5625124
Publication date: 1971
Functionals in proof theory (03F10) Proof theory in general (including proof-theoretic semantics) (03F03) Relative consistency and interpretations (03F25)
Related Items
Classical logic, storage operators and second-order lambda-calculus, Typed equivalence, type assignment, and type containment, A general storage theorem for integers in call-by-name \(\lambda\)- calculus, Cut-elimination for quantified conditional logic, Inductively defined types in the Calculus of Constructions, Algebraic types in PER models, On the Versatility of Open Logical Relations, Applications of type theory, Dependent choice, `quote' and the clock, A characterization of F-complete type assignments, The system \({\mathcal F}\) of variable types, fifteen years later, Unnamed Item, Higher-order unification with dependent function types, Adding algebraic rewriting to the untyped lambda calculus (extended abstract), Programming and Proving with Classical Types, Algebraic proofs of cut elimination, Combinatory logic with polymorphic types, Adequacy for a lazy functional language with recursive and polymorphic types, Paths-based criteria and application to linear logic subsystems characterizing polynomial time, On Paths-Based Criteria for Polynomial Time Complexity in Proof-Nets, Inductive types and type constraints in the second-order lambda calculus, A strong normalization result for classical logic, The calculus of constructions, Toposes and intuitionistic theories of types, Lambda-calcul, évaluation paresseuse et mise en mémoire, On Church's formal theory of functions and functionals. The \(\lambda\)- calculus: Connections to higher type recursion theory, proof theory, category theory, An extension of system F with subtyping, A Survey of the Proof-Theoretic Foundations of Logic Programming, A domain-theoretic semantics of lax generic functions., Phase semantics for light linear logic, Choice and independence of premise rules in intuitionistic set theory, Termination of rewrite relations on \(\lambda\)-terms based on Girard's notion of reducibility, The existential fragment of second-order propositional intuitionistic logic is undecidable, Reduction Free Normalisation for a proof irrelevant type of propositions, Realizability algebras III: some examples, Types, abstraction, and parametric polymorphism, part 2, A rationale for conditional equational programming, A Constructive Semantic Approach to Cut Elimination in Type Theories with Axioms, Recursion over realizability structures, On strong normalization and type inference in the intersection type discipline, Behavioural inverse limit \(\lambda\)-models, Metacircularity in the polymorphic \(\lambda\)-calculus, A Type Theory for Probabilistic $$\lambda $$–calculus, Graded modal dependent type theory, Proving properties of typed \(\lambda\)-terms using realizability, covers, and sheaves, Bounded linear logic: A modular approach to polynomial-time computability, Adjectival and adverbial modification: the view from modern type theories, Deverbal semantics and the Montagovian generative lexicon \(\Lambda \mathsf {Ty}_n\), Strong normalization from an unusual point of view, Adding algebraic rewriting to the untyped lambda calculus, Constructive logics. I: A tutorial on proof systems and typed \(\lambda\)- calculi, Natural language inference in Coq, Uniform Heyting arithmetic, Unnamed Item, Linear logic, On the expressive power of schemes, Unnamed Item, A relational account of call-by-value sequentiality, Burali-Forti as a purely logical paradox, Inductive-data-type systems, Unnamed Item, Prawitz, Proofs, and Meaning, Operations on records, Typing and computational properties of lambda expressions, Building continuous webbed models for system F, Mechanized metatheory revisited, Cut-elimination for a logic with definitions and induction, A simple proof of second-order strong normalization with permutative conversions, Typing untyped \(\lambda\)-terms, or reducibility strikes again!, From computation to foundations via functions and application: The \(\lambda\)-calculus and its webbed models, Program Testing and the Meaning Explanations of Intuitionistic Type Theory, Term-generic logic, On Takeuti's early view of the concept of set, Type-directed specialization of polymorphism., A sequent calculus for subtyping polymorphic types, On the Convergence of Reduction-based and Model-based Methods in Proof Theory, Free Theorems and Runtime Type Representations, Cogent: uniqueness types and certifying compilation, Computational foundations of basic recursive function theory, The genericity theorem and parametricity in the polymorphic \(\lambda\)- calculus, A note on subject reduction in \((\to, \exists)\)-Curry with respect to complete developments, Neo-Logicism and Its Logic, A selected bibliography on constructive mathematics, intuitionistic type theory and higher order deduction
