| 1. |
- Abel, Andreas, 1974, et al.
(författare)
-
Normalization by evaluation in the delay monad: A case study for coinduction via copatterns and sized types
- 2014
-
Ingår i: Electronic Proceedings in Theoretical Computer Science, EPTCS. - 2075-2180.
-
Konferensbidrag (refereegranskat)abstract
- In this paper, we present an Agda formalization of a normalizer for simply-typed lambda terms. The normalizer consists of two coinductively defined functions in the delay monad: One is a standard evaluator of lambda terms to closures, the other a type-directed reifier from values to h-long b-normal forms. Their composition, normalization-by-evaluation, is shown to be a total function a posteriori, using a standard logical-relations argument. The successful formalization serves as a proof-of-concept for coinductive programming and reasoning using sized types and copatterns, a new and presently experimental feature of Agda.
|
|
| 2. |
- Adams, Robin, 1978
(författare)
-
QPEL: Quantum Program and Effect Language
- 2014
-
Ingår i: Electronic Proceedings in Theoretical Computer Science. - 2075-2180. ; 172, s. 133-153
-
Konferensbidrag (refereegranskat)abstract
- We present the syntax and rules of deduction of QPEL (Quantum Program and Effect Language), a language for describing both quantum programs, and properties of quantum programs - effects on the appropriate Hilbert space. We show how semantics may be given in terms of state-and-effect triangles, a categorical setting that allows semantics in terms of Hilbert spaces, C*-algebras, and other categories. We prove soundness and completeness results that show the derivable judgements are exactly those provable in all state-and-effect triangles.
|
|
| 3. |
- Mannaa, Bassel, 1982, et al.
(författare)
-
A Sheaf Model of the Algebraic Closure
- 2014
-
Ingår i: Proceedings Fifth International Workshop on Classical Logic and Computation (CL&C 2014), Vienna, Austria, July 13, 2014, EPTCS. - 2075-2180. ; 164, s. 18-32
-
Konferensbidrag (refereegranskat)abstract
- In constructive algebra one cannot in general decide the irreducibility of a polynomial over a field K. This poses some problems to showing the existence of the algebraic closure of K. We give a possible constructive interpretation of the existence of the algebraic closure of a field in characteristic 0 by building, in a constructive metatheory, a suitable site model where there is such an algebraic closure. One can then extract computational content from this model. We give examples of computation based on this model.
|
|
| 4. |
- Martínez, Enrique, et al.
(författare)
-
Timed Automata Semantics for Visual e-Contracts
- 2011
-
Ingår i: EPTCS. - 2075-2180. ; 68, s. 7-21
-
Konferensbidrag (refereegranskat)abstract
- C-O Diagrams have been introduced as a means to have a more visual representation of electronic contracts, where it is possible to represent the obligations, permissions and prohibitions of the different signatories, as well as what are the penalties in case of not fulfillment of their obligations and prohibitions. In such diagrams we are also able to represent absolute and relative timing constraints. In this paper we present a formal semantics for C-O Diagrams based on timed automata extended with an ordering of states and edges in order to represent different deontic modalities.
|
|
| 5. |
- Montazeri, Seyed, et al.
(författare)
-
From Contracts in Structured English to CL Specifications
- 2011
-
Ingår i: EPTCS. - 2075-2180. ; 68, s. 55-69
-
Konferensbidrag (refereegranskat)abstract
- In this paper we present a framework to analyze conflicts of contracts written in structured English. A contract that has manually been rewritten in a structured English is automatically translated into a formal language using the Grammatical Framework (GF). In particular we use the contract language CL as a target formal language for this translation. In our framework CL specifications could then be input into the tool CLAN to detect the presence of conflicts (whether there are contradictory obligations, permissions, and prohibitions. We also use GF to get a version in (restricted) English of CL formulae. We discuss the implementation of such a framework.
|
|
