scientific article; zbMATH DE number 512777

MaRDI QIDQ4281470zbMATH OpenFDO

Authors Gilles Dowek

Publication date 9 June 1994

zbMATH Keywords

\(\lambda\)-calculus\(\lambda\)-Prologprogramming language ELFtype inference algorithm

Mathematics Subject Classification ID

Decidability of theories and sets of sentences (03B25) Combinatory logic and lambda calculus (03B40) Theory of programming languages (68N15) Logic programming (68N17)

Recommendations

• Undecidability of Type-Checking in Domain-Free Typed Lambda-Calculi with Existence
• scientific article; zbMATH DE number 512796
• Typability and type checking in System F are equivalent and undecidable

Cited in

(14)

• Comparing cubes of typed and type assignment systems
• The underdetermination of typings
• Communication errors in the \(\pi\)-calculus are undecidable
• \texttt{slepice}: towards a verified implementation of type theory in type theory
• A simple proof of the undecidability of inhabitation in λP
• scientific article; zbMATH DE number 29189 (Why is no real title available?)
• scientific article; zbMATH DE number 626035 (Why is no real title available?)
• scientific article; zbMATH DE number 1512625 (Why is no real title available?)
• Theoretical Pearls:Representing ‘undefined’ in lambda calculus
• Introduction to Type Theory
• Elf: A meta-language for deductive systems
• THE UNDECIDABILITY OF TYPE RELATED PROBLEMS IN TYPE -FREE STYLE SYSTEM F
• Undecidability of 2-Label BPP Equivalences and Behavioral Type Systems for the π-Calculus
• Sharing proofs with predicative theories through universe-polymorphic elaboration

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 Q4281470)