Encoding monomorphic and polymorphic types

DOI10.1007/978-3-642-36742-7_34MaRDI QIDQ5326348zbMATH OpenOpenAlexFDO

Authors Jasmin Christian Blanchette, Sascha Böhme, Andrei Popescu, Nicholas Smallbone

Publication date 5 August 2013

Published in Tools and Algorithms for the Construction and Analysis of Systems (Search for Journal in Brave)

Full work available at URL https://eprints.mdx.ac.uk/15166/1/TACAS2013.pdf

Mathematics Subject Classification ID

Recommendations

• Encoding monomorphic and polymorphic types
• Optimized encodings of fragments of type theory in first order logic
• Expressing polymorphic types in a many-sorted language
• Handling Polymorphism in Automated Deduction
• TFF1: The TPTP Typed First-Order Form with Rank-1 Polymorphism

Cited in

(18)

• A formalized general theory of syntax with bindings: extended version
• Finding Finite Models in Multi-sorted First-Order Logic
• Encoding types in ML-like languages
• The higher-order prover \textsc{Leo}-II
• Semi-intelligible Isar proofs from machine-generated proofs
• Handling Polymorphism in Automated Deduction
• Efficient encodings of first-order Horn formulas in equational logic
• Encoding monomorphic and polymorphic types
• Soundly proving B method formulæ using typed sequent calculus
• A Polymorphic Vampire
• GRUNGE: a grand unified ATP challenge
• Expressing polymorphic types in a many-sorted language
• Extending Sledgehammer with SMT solvers
• A learning-based fact selector for Isabelle/HOL
• Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)
• A formalized general theory of syntax with bindings
• HOL(y)Hammer: online ATP service for HOL Light
• Soundness and completeness proofs by coinductive methods

Describes a project that uses

Uses Software

• Isabelle/HOL
• MPTP 0.2
• Why3

This page was built for publication: Encoding monomorphic and polymorphic types

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