Translating a Dependently-Typed Logic to First-Order Logic
From MaRDI portal
Publication:3184740
DOI10.1007/978-3-642-03429-9_21zbMath1253.03100MaRDI QIDQ3184740
Florian Rabe, Kristina Sojakova
Publication date: 22 October 2009
Published in: Recent Trends in Algebraic Development Techniques (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-642-03429-9_21
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Investigations in many-sorted quantor logic
- Isabelle. A generic theorem prover
- CASL: the Common Algebraic Specification Language.
- Dependently Sorted Logic
- Combining Type Theory and Untyped Set Theory
- First-Order Logic with Dependent Types
- A framework for defining logics
- Institutions: abstract model theory for specification and programming