Domain-Freeλµ-Calculus

DOI10.1051/ita:2000102zbMath0974.68032OpenAlexW2053001507MaRDI QIDQ2729625

Ken-etsu Fujita

Publication date: 12 December 2001

Published in: RAIRO - Theoretical Informatics and Applications (Search for Journal in Brave)

Full work available at URL: https://eudml.org/doc/222038

zbMATH Keywords

domain-free \(\lambda\mu\)-calculus

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Combinatory logic and lambda calculus (03B40)

Related Items (8)

Strong normalization proofs by CPS-translations ⋮ Existential type systems between Church and Curry style (type-free style) ⋮ Strong normalization proof with CPS-translation for second order classical natural deduction ⋮ The undecidability of type related problems in the type-free style System F with finitely stratified polymorphic types ⋮ Strong normalization of classical natural deduction with disjunctions ⋮ Confluence proofs of lambda-mu-calculi by Z theorem ⋮ CPS-translation as adjoint ⋮ Confluency and strong normalizability of call-by-value \(\lambda \mu\)-calculus

Uses Software

• ML
• Automath
• MiniML

Cites Work

• Notions of computation and monads
• Recursive unsolvability of Post's problem of Tag und other topics in theory of Turing machines
• The lambda calculus. Its syntax and semantics. Rev. ed.
• Polymorphic type inference and containment
• Call-by-name, call-by-value and the \(\lambda\)-calculus
• A theory of type polymorphism in programming
• Monad as modality
• Corrigendum: Polymorphic type assignment and CPS conversion
• Church-Rosser property of a simple reduction for full first-order classical natural deduction
• A normalization-procedure for the first order classical natural deduction with full logical symbols
• A modal analysis of staged computation
• Classical logic, continuation semantics and abstract machines
• An analysis of ML typability
• Proofs of strong normalisation for second order classical natural deduction
• Domain-free pure type systems
• Sound and complete axiomatisations of call-by-value control operators
• Turing machines with restricted memory access
• Parallel reductions in \(\lambda\)-calculus
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Domain-Freeλµ-Calculus