scientific article
From MaRDI portal
Publication:3077958
zbMath1347.03001MaRDI QIDQ3077958
Wil Dekkers, Richard Statman, Hendrik Pieter Barendregt
Publication date: 18 February 2011
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
Introductory exposition (textbooks, tutorial papers, etc.) pertaining to mathematical logic and foundations (03-01) Logic in computer science (03B70) Combinatory logic and lambda calculus (03B40) Abstract and axiomatic computability and recursion theory (03D75)
Related Items (55)
A type assignment for \(\lambda\)-calculus complete both for FPTIME and strong normalization ⋮ Levy Labels and Recursive Types ⋮ Soundness Conditions for Big-Step Semantics ⋮ On sets of terms having a given intersection type ⋮ Unnamed Item ⋮ Combinatory logic with polymorphic types ⋮ From realizability to induction via dependent intersection ⋮ Nominal essential intersection types ⋮ Parametric Church's thesis: synthetic computability without choice ⋮ Monotone recursive types and recursive data representations in Cedille ⋮ Semantics of quantum programming languages: Classical control, quantum control ⋮ Extensional higher-order paramodulation in Leo-III ⋮ A Survey of the Proof-Theoretic Foundations of Logic Programming ⋮ When programs have to watch paint dry ⋮ Fixed points in lambda calculus. an eccentric survey of problems and solutions ⋮ From semantics to types: the case of the imperative \(\lambda\)-calculus ⋮ Type inference for rank-2 intersection types using set unification ⋮ Rensets and renaming-based recursion for syntax with bindings extended version ⋮ Typed path polymorphism ⋮ Structural rules and algebraic properties of intersection types ⋮ A Computable Solution to Partee’s Temperature Puzzle ⋮ Node Replication: Theory And Practice ⋮ On some enumerative problems in lambda calculus ⋮ Unnamed Item ⋮ A characterization of lambda-terms transforming numerals ⋮ First-order automated reasoning with theories: when deduction modulo theory meets practice ⋮ The untyped computational \(\lambda \)-calculus and its intersection type discipline ⋮ Unnamed Item ⋮ The Cooper storage idiom ⋮ Unnamed Item ⋮ Metric Reasoning About $$\lambda $$-Terms: The General Case ⋮ The New Normal: We Cannot Eliminate Cuts in Coinductive Calculi, But We Can Explore Them ⋮ Mathematical logic: proof theory, constructive mathematics. Abstracts from the workshop held November 5--11, 2017 ⋮ A coinductive approach to proof search through typed lambda-calculi ⋮ The spirit of node replication ⋮ How to think of intersection types as Cartesian products ⋮ Strong normalization through intersection types and memory ⋮ Clocks for Functional Programs ⋮ Composition and decomposition of multiparty sessions ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Obituary: Nicolaas Govert de Bruijn (1918--2012). Mathematician, computer scientist, logician ⋮ De Bruijn's weak diamond property revisited ⋮ A Coalgebraic View of Bar Recursion and Bar Induction ⋮ Unnamed Item ⋮ Automating free logic in HOL, with an experimental application in category theory ⋮ COCHIS: Stable and coherent implicits ⋮ Agent-Based HOL Reasoning ⋮ A Generic Framework for Higher-Order Generalizations. ⋮ On implicational intermediate logics axiomatizable by formulas minimal in classical logic: a counter-example to the Komori-Kashima problem ⋮ Inhabitation in simply typed lambda-calculus through a lambda-calculus for proof search ⋮ Unnamed Item ⋮ Almost all Classical Theorems are Intuitionistic
This page was built for publication:
