Expressing Polymorphic Types in a Many-Sorted Language

DOI10.1007/978-3-642-24364-6_7zbMath1348.68215OpenAlexW1566741425MaRDI QIDQ3172884

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

Mathematics Subject Classification ID

Logic in computer science (03B70)

Related Items (6)

A Polymorphic Vampire ⋮ Expressing Polymorphic Types in a Many-Sorted Language ⋮ Unnamed Item ⋮ Encoding Monomorphic and Polymorphic Types ⋮ Axiomatization of Typed First-Order Logic ⋮ A combinator-based superposition calculus for higher-order logic

Uses Software

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

Cites Work

• Unnamed Item
• Unnamed Item
• Isabelle/HOL. A proof assistant for higher-order logic
• Translating higher-order clauses to first-order clauses
• Expressing Polymorphic Types in a Many-Sorted Language
• A Polymorphic Intermediate Verification Language: Design and Logical Encoding
• Handling Polymorphism in Automated Deduction

This page was built for publication: Expressing Polymorphic Types in a Many-Sorted Language