In Praise of Impredicativity: A Contribution to the Formalization of Meta-Programming

DOI10.1017/S1471068419000024zbMath1434.68102arXiv1807.06051OpenAlexW3102367795MaRDI QIDQ5108530

François Bry

Publication date: 4 May 2020

Published in: Theory and Practice of Logic Programming (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/1807.06051

zbMATH Keywords

reflectionmodel theorylogic programmingRussell's paradoxmeta-programmingbarber paradox

Mathematics Subject Classification ID

Logic in computer science (03B70) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items

An Asymptotic Analysis of Probabilistic Logic Programming, with Implications for Expressing Projective Families of Distributions, Unnamed Item

Uses Software

• ML
• HiLog
• Twelf
• Automath

Cites Work

• Languages with self-reference. I: Foundations (or: We can have everything in first-order logic!)
• Languages with self-reference. II: Knowledge, belief, and modality
• Prolegomena to a theory of mechanized formal reasoning
• A theory of type polymorphism in programming
• On the logic of common belief and common knowledge
• Untersuchungen über das logische Schliessen. I
• On the undecidability of second-order unification
• One hundred years of Russell's paradox. Mathematics, logic, philosophy. Based on the Munich centenary conference, Munich, Germany, June 2001.
• Programming with Higher-Order Logic
• Extensional Higher-Order Logic Programming
• Contributions to the Theory of Logic Programming
• A framework for defining logics
• HiLog: A foundation for higher-order logic programming
• The Semantics of Predicate Logic as a Programming Language
• Combining negation as failure and embedded implications in logic programs
• A metalogic programming approach: language, semantics and applications
• Reflection principles in computational logic
• A logical analysis of modules in logic programming
• On the declarative and procedural semantics of definite metalogic programs
• Modules for Prolog Revisited
• Flow diagrams, turing machines and languages with only two formation rules
• The Principal Type-Scheme of an Object in Combinatory Logic
• Letter to the Editor
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item