Skip to Main content Skip to Navigation
Conference papers

Compiling Logics

Abstract : We present an architecture that permits compiling declarative logic specifications (given in some type theory like LF) into implementations of that logic within the Heterogeneous Tool Set Hets. The central contributions are the use of declaration patterns for singling out a suitable subset of signatures for a particular logic, and the automatic generation of datatypes and functions for parsing and static analysis of declaratively specified logics.
Document type :
Conference papers
Complete list of metadata

Cited literature [19 references]  Display  Hide  Download

https://hal.inria.fr/hal-01485981
Contributor : Hal Ifip <>
Submitted on : Thursday, March 9, 2017 - 3:33:46 PM
Last modification on : Thursday, June 4, 2020 - 6:24:02 PM
Long-term archiving on: : Saturday, June 10, 2017 - 2:42:24 PM

File

978-3-642-37635-1_7_Chapter.pd...
Files produced by the author(s)

Licence


Distributed under a Creative Commons Attribution 4.0 International License

Identifiers

Citation

Mihai Codescu, Fulya Horozal, Aivaras Jakubauskas, Till Mossakowski, Florian Rabe. Compiling Logics. 21th InternationalWorkshop on Algebraic Development Techniques (WADT), Jun 2012, Salamanca, Spain. pp.111-126, ⟨10.1007/978-3-642-37635-1_7⟩. ⟨hal-01485981⟩

Share

Metrics

Record views

584

Files downloads

281