scientific article; zbMATH DE number 1512625

zbMATH Open0961.68032MaRDI QIDQ4508310FDOQ4508310

Authors: Aleksy Schubert 

Publication date: 3 October 2000

Title of this publication is not available (Why is that?)

Recommendations

• Proof-relevant Horn clauses for dependent type inference and term synthesis
• scientific article; zbMATH DE number 445157
• Higher-order unification with dependent function types
• scientific article; zbMATH DE number 512777
• scientific article; zbMATH DE number 18625

zbMATH Keywords

decidabilitytype inference

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Classical first-order logic (03B10) Decidability of theories and sets of sentences (03B25) Combinatory logic and lambda calculus (03B40)

Cited In (4)

• Proof-relevant Horn clauses for dependent type inference and term synthesis
• Title not available (Why is that?)
• Optimized encodings of fragments of type theory in first order logic
• An Expressive First-Order Logic with Flexible Typing for Natural Language Semantics

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