scientific article; zbMATH DE number 1512625

MaRDI QIDQ4508310zbMATH OpenFDO

Authors Aleksy Schubert

Publication date 3 October 2000

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)

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

Cited in

(4)

• scientific article; zbMATH DE number 4092733 (Why is no real title available?)
• Optimized encodings of fragments of type theory in first order logic
• Proof-relevant Horn clauses for dependent type inference and term synthesis
• 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)