Expressing polymorphic types in a many-sorted language

DOI10.1007/978-3-642-24364-6_7zbMATH Open1348.68215OpenAlexW1566741425MaRDI QIDQ3172884FDOQ3172884

Andrei Paskevich, François Bobot

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

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

Mathematics Subject Classification ID

Logic in computer science (03B70)

Cites Work

• Isabelle/HOL. A proof assistant for higher-order logic
• Translating higher-order clauses to first-order clauses
• Title not available (Why is that?)
• Title not available (Why is that?)
• Expressing Polymorphic Types in a Many-Sorted Language
• A Polymorphic Intermediate Verification Language: Design and Logical Encoding
• Handling Polymorphism in Automated Deduction

Cited In (8)

• Sorting Multidimensional Types: Theory and Application
• Polytypic values possess polykinded types
• Title not available (Why is that?)
• A combinator-based superposition calculus for higher-order logic
• Axiomatization of Typed First-Order Logic
• Expressing Polymorphic Types in a Many-Sorted Language
• Encoding Monomorphic and Polymorphic Types
• A Polymorphic Vampire

Uses Software

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

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)