Expressing polymorphic types in a many-sorted language

DOI10.1007/978-3-642-24364-6_7MaRDI QIDQ3172884zbMATH OpenOpenAlexFDO

Authors François Bobot, Andrei Paskevich

Publication date 7 October 2011

Published in Frontiers of Combining Systems (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-24364-6_7

Mathematics Subject Classification ID

Logic in computer science (03B70)

Recommendations

• Handling Polymorphism in Automated Deduction
• Encoding monomorphic and polymorphic types
• Encoding monomorphic and polymorphic types
• Sort it out with monotonicity. Translating between many-sorted and unsorted first-order logic
• Optimized encodings of fragments of type theory in first order logic

Cites work

• scientific article; zbMATH DE number 2090293 (Why is no real title available?)
• scientific article; zbMATH DE number 824731 (Why is no real title available?)
• A polymorphic intermediate verification language: design and logical encoding
• Expressing polymorphic types in a many-sorted language
• Handling Polymorphism in Automated Deduction
• Isabelle/HOL. A proof assistant for higher-order logic
• Translating higher-order clauses to first-order clauses

Cited in

(11)

• Sorting Multidimensional Types: Theory and Application
• Polytypic values possess polykinded types
• scientific article; zbMATH DE number 7350767 (Why is no real title available?)
• A combinator-based superposition calculus for higher-order logic
• Expressing polymorphic types in a many-sorted language
• Encoding monomorphic and polymorphic types
• Sort it out with monotonicity. Translating between many-sorted and unsorted first-order logic
• Encoding monomorphic and polymorphic types
• Handling Polymorphism in Automated Deduction
• Axiomatization of typed first-order logic
• A Polymorphic Vampire

Describes a project that uses

Uses Software

• Jessie
• z3
• cvc3
• Frama-C
• Metis
• Why3
• Yices
• SMT-LIB
• VAMPIRE
• Isabelle/HOL
• ML
• Coq

This page was built for publication: Expressing polymorphic types in a many-sorted language

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3172884)