Deprecated: $wgMWOAuthSharedUserIDs=false is deprecated, set $wgMWOAuthSharedUserIDs=true, $wgMWOAuthSharedUserSource='local' instead [Called from MediaWiki\HookContainer\HookContainer::run in /var/www/html/w/includes/HookContainer/HookContainer.php at line 135] in /var/www/html/w/includes/Debug/MWDebug.php on line 372
A UNIFICATION ALGORITHM FOR THE λΠ-CALCULUS - MaRDI portal

A UNIFICATION ALGORITHM FOR THE λΠ-CALCULUS

From MaRDI portal

Publication:5286030

Jump to:navigation, search

DOI10.1142/S012905419200019XzbMath0784.03013MaRDI QIDQ5286030

David J. Pym

Publication date: 29 June 1993

Published in: International Journal of Foundations of Computer Science (Search for Journal in Brave)

zbMATH Keywords

higher-order logic unification lambda calculus dependent types logical frameworks contextual categories

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42) Combinatory logic and lambda calculus (03B40)

Related Items (7)

A note on the proof theory of the \(\lambda \Pi\)-calculus ⋮ The Alf proof editor and its proof engine ⋮ Equivalences between logics and their representing type theories ⋮ An algorithm for checking incomplete proof objects in type theory with localization and unification ⋮ Proof-term synthesis on dependent-type systems via explicit substitutions ⋮ Proof-search in type-theoretic languages: An introduction ⋮ The practice of logical frameworks

This page was built for publication: A UNIFICATION ALGORITHM FOR THE λΠ-CALCULUS

Retrieved from "https://portal.mardi4nfdi.de/w/index.php?title=Publication:5286030&oldid=19941203"