scientific article; zbMATH DE number 5852776
From MaRDI portal
Publication:3077958
Recommendations
- The lambda calculus. Its syntax and semantics. Rev. ed.
- scientific article; zbMATH DE number 4002064
- scientific article; zbMATH DE number 783760
- scientific article; zbMATH DE number 5318491
- scientific article; zbMATH DE number 2242116
- scientific article; zbMATH DE number 3875232
- scientific article; zbMATH DE number 4024773
- scientific article; zbMATH DE number 46869
- scientific article; zbMATH DE number 42059
- The Impact of the Lambda Calculus in Logic and Computer Science
Cited in
(78)- Nominal essential intersection types
- Fixed points in lambda calculus. an eccentric survey of problems and solutions
- The Cooper storage idiom
- Mathematical logic: proof theory, constructive mathematics. Abstracts from the workshop held November 5--11, 2017
- How to think of intersection types as Cartesian products
- Strong normalization through intersection types and memory
- Composition and decomposition of multiparty sessions
- On implicational intermediate logics axiomatizable by formulas minimal in classical logic: a counter-example to the Komori-Kashima problem
- Combinatory logic with polymorphic types
- Parametric Church's thesis: synthetic computability without choice
- Semantics of quantum programming languages: Classical control, quantum control
- On some enumerative problems in lambda calculus
- First-order automated reasoning with theories: when deduction modulo theory meets practice
- The untyped computational \(\lambda \)-calculus and its intersection type discipline
- A coinductive approach to proof search through typed lambda-calculi
- The spirit of node replication
- Automating free logic in HOL, with an experimental application in category theory
- Typed path polymorphism
- From realizability to induction via dependent intersection
- Extensional higher-order paramodulation in Leo-III
- A type assignment for -calculus complete both for FPTIME and strong normalization
- Types and programing languages
- A coalgebraic view of bar recursion and bar induction
- Agent-based HOL reasoning
- Type theory and formal proof. An introduction
- A Computable Solution to Partee’s Temperature Puzzle
- Metric reasoning about -terms: the general case
- Revisiting call-by-value Böhm trees in light of their Taylor expansion
- scientific article; zbMATH DE number 5318491 (Why is no real title available?)
- scientific article; zbMATH DE number 4058907 (Why is no real title available?)
- scientific article; zbMATH DE number 177773 (Why is no real title available?)
- scientific article; zbMATH DE number 1342246 (Why is no real title available?)
- Efficient type checking for path polymorphism
- Relational graph models at work
- scientific article; zbMATH DE number 7029315 (Why is no real title available?)
- COCHIS: stable and coherent implicits
- Strong typed Böhm theorem and functional completeness on the linear lambda calculus
- Soundness conditions for big-step semantics
- On sets of terms having a given intersection type
- Monotone recursive types and recursive data representations in Cedille
- A Generic Framework for Higher-Order Generalizations.
- The -calculus: syntax and types
- scientific article; zbMATH DE number 7204434 (Why is no real title available?)
- Gems of Corrado Böhm
- The new normal: we cannot eliminate cuts in coinductive calculi, but we can explore them
- Inhabitation in simply typed lambda-calculus through a lambda-calculus for proof search
- Levy labels and recursive types
- A characterization of lambda-terms transforming numerals
- Clocks for Functional Programs
- Almost all Classical Theorems are Intuitionistic
- Lower end of the linial-post spectrum
- A Survey of the Proof-Theoretic Foundations of Logic Programming
- When programs have to watch paint dry
- scientific article; zbMATH DE number 7756108 (Why is no real title available?)
- 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
- Structural rules and algebraic properties of intersection types
- Node Replication: Theory And Practice
- A type-based HFL model checking algorithm
- Canonicity of proofs in constructive modal logic
- One or nothing: anti-unification over the simply-typed lambda calculus
- From semantics to types: the case of the imperative \(\lambda\)-calculus
- Linear additives
- Pregrammars and intersection types
- A type checker for a logical framework with union and intersection types (system description)
- Mechanized HOL reasoning in set theory
- Substitution for non-wellfounded syntax with binders through monoidal categories
- Mechanized subject expansion in uniform intersection types for perpetual reductions
- A new conjecture about identity of proofs
- Asymptotic distribution of parameters in trivalent maps and linear lambda terms
- Intersection types for a computational lambda-calculus with global state
- A generic deskolemization strategy
- YACC: Yet Another Church Calculus. A birthday present for Herman inspired by his supervisor activity
- -symsym: an interactive tool for playing with involutions and types
- From proof-theoretic validity to base-extension semantics for intuitionistic propositional logic
- Obituary: Nicolaas Govert de Bruijn (1918--2012). Mathematician, computer scientist, logician
- De Bruijn's weak diamond property revisited
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 Q3077958)
