Kripke semantics for higher-order type theory applied to constraint logic programming languages

DOI10.1016/j.tcs.2017.11.005zbMath1387.68059MaRDI QIDQ683712

James Lipton, Susana Nieva

Publication date: 9 February 2018

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.tcs.2017.11.005

zbMATH Keywords

higher-order logic; Kripke models; constraint logic programming; typed \(\lambda\)-calculus

Mathematics Subject Classification ID

68N17: Logic programming

Uses Software

• HiLog
• Hiord
• Ciao
• CiaoPP
• CoALP

Cites Work

• Coalgebras in functional programming and type theory
• Kripke-style models for typed lambda calculus
• Abstraction-carrying code: a model for mobile code safety
• On the algebraic structure of declarative programming languages
• Focusing and polarization in linear, intuitionistic, and classical logics
• Constructivism in mathematics. An introduction. Volume I
• A semantics for \(\lambda \)Prolog
• A theory of observables for logic programs
• A proof of cut-elimination theorem in simple type-theory
• Integrated program debugging, verification, and optimization using abstract interpretation (and the Ciao system preprocessor)
• Uniform proofs as a foundation for logic programming
• Coinductive Constraint Logic Programming
• Kripke Semantics for Martin-L\"of's Extensional Type Theory
• Completeness and Cut-elimination in the Intuitionistic Theory of Types
• Analyzing security protocols with secrecy types and logic programs
• Higher-Order Logic Programming Languages with Constraints: A Semantics
• N-Prolog: An extension of Prolog with hypothetical implications. I.
• Logic Programming with Focusing Proofs in Linear Logic
• HiLog: A foundation for higher-order logic programming
• Constraint Logic Programming with Hereditary Harrop formulas
• A logical analysis of modules in logic programming
• Higher-order semantics and extensionality
• Formalizing a Constraint Deductive Database Language Based on Hereditary Harrop Formulas with Negation
• Advances in Computer Science - ASIAN 2004. Higher-Level Decision Making
• Resolution in type theory
• The completeness of the first-order functional calculus
• Completeness in the theory of types
• FSTTCS 2005: Foundations of Software Technology and Theoretical Computer Science
• Logic and structure
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item