Abstract deduction and inferential models for type theory

DOI10.1016/j.ic.2010.03.002zbMath1197.03034OpenAlexW1975424061MaRDI QIDQ988551

Maurizio Martelli, Paolo Gentilini

Publication date: 18 August 2010

Published in: Information and Computation (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.ic.2010.03.002

zbMATH Keywords

proof theorylogic in computer scienceconstructive semantics for higher-order logic

Mathematics Subject Classification ID

Uses Software

• ETPS

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Linear logic
• Kripke-style models for typed lambda calculus
• Proof theory. 2nd ed
• A semantics for \(\lambda \)Prolog
• Untersuchungen über das logische Schliessen. I
• Proof-theoretic modal PA-completeness. I: A system-sequent metric
• Proof-theoretic modal PA-completeness. II: The syntactic countermodel
• Proof-theoretic modal PA-completeness. III: The syntactic proof
• Uniform proofs as a foundation for logic programming
• Completeness and Cut-elimination in the Intuitionistic Theory of Types
• A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification
• The s-semantics approach: Theory and applications
• Hauptsatz for higher order logic
• Resolution in type theory
• General models and extensionality
• Completeness in the theory of types

This page was built for publication: Abstract deduction and inferential models for type theory