Name
Abstract | ||
|---|---|---|
Logical frameworks like LF are used for formal representations of logics in order to make them amenable to formal machine-assisted meta-reasoning. While the focus has originally been on logics with a proof theoretic semantics, we have recently shown how to define model theoretic logics in LF as well. We have used this to define new institutions in the Heterogeneous Tool Set in a purely declarative way. It is desirable to extend this model theoretic representation of logics to the level of structured specifications. Here a particular challenge among structured specification building operations is hiding, which restricts a specification to some export interface. Specification languages like ASL and CASL support hiding, using an institution-independent model theoretic semantics abstracting from the details of the underlying logical system. Logical frameworks like LF have also been equipped with structuring languages. However, their proof theoretic nature leads them to a theory-level semantics without support for hiding. In the present work, we show how to resolve this difficulty. |
Year | DOI | Venue |
|---|---|---|
2010 | 10.1007/978-3-642-28412-0_9 | WADT |
Keywords | Field | DocType |
institution-independent model theoretic semantics,casl support hiding,model theoretic representation,specification language,proof theoretic interpretation,proof theoretic nature,logical framework,structured specification,proof theoretic semantics,structured specification building operation,model theoretic logic,model theoretic hiding | Proof-theoretic semantics,Computer science,Algorithm,Theoretical computer science,Structuring,Type family,Logical framework,Semantics | Conference |
Citations | PageRank | References |
2 | 0.38 | 19 |
Authors | ||
5 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Mihai Codescu | 1 | 89 | 12.58 |
| Fulya Horozal | 2 | 55 | 4.32 |
| Michael Kohlhase | 3 | 1095 | 127.65 |
| Till Mossakowski | 4 | 1052 | 90.11 |
| Florian Rabe | 5 | 333 | 41.66 |