Sciweavers

FUIN
2010
156views more  FUIN 2010»
13 years 10 months ago
A Tutorial Implementation of a Dependently Typed Lambda Calculus
Abstract. We present the type rules for a dependently typed core calculus together with a straightforward implementation in Haskell. We explicitly highlight the changes necessary t...
Andres Löh, Conor McBride, Wouter Swierstra
ENTCS
2000
114views more  ENTCS 2000»
13 years 11 months ago
Syntactic Type Soundness for the Region Calculus
The region calculus of Tofte and Talpin is an annotated polymorphically typed lambda calculus which makes memory allocation and deallocation explicit. It is intended as an interme...
Simon Helsen, Peter Thiemann
APAL
2008
79views more  APAL 2008»
13 years 11 months ago
Parameter-free polymorphic types
Consider the following restriction of the polymorphically typed lambda calculus ("System F"). All quantifications are parameter free. In other words, in every universal ...
Klaus Aehlig
ACL
2003
14 years 26 days ago
A Computational Treatment of Korean Temporal Markers, OE and DONGAN
In this paper, we elucidate how Korean temporal markers, OE and DONGAN contribute to specifying the event time and formalize it in terms of typed lambda calculus. We also present ...
Hyunjung Son
ACL
2006
14 years 26 days ago
Translating HPSG-Style Outputs of a Robust Parser into Typed Dynamic Logic
The present paper proposes a method by which to translate outputs of a robust HPSG parser into semantic representations of Typed Dynamic Logic (TDL), a dynamic plural semantics de...
Manabu Sato, Daisuke Bekki, Yusuke Miyao, Jun-ichi...
CTCS
1987
Springer
14 years 3 months ago
A Typed Lambda Calculus with Categorical Type Constructors
A typed lambda calculus with categorical type constructors is introduced. It has a uniform category theoretic mechanism to declare new types. Its type structure includes categoric...
Tatsuya Hagino
FOSSACS
2000
Springer
14 years 3 months ago
Constructive Data Refinement in Typed Lambda Calculus
A new treatment of data refinement in typed lambda calculus is proposed, phrased in terms of pre-logical relations [HS99] rather than logical relations, and incorporating a constru...
Furio Honsell, John Longley, Donald Sannella, Andr...
FPCA
1989
14 years 3 months ago
A Simple Semantics for ML Polymorphism
We give a framework for denotational semantics for the polymorphic “core” of the programming language ML. This framework requires no more semantic material than what is needed...
Atsushi Ohori
TAPSOFT
1997
Springer
14 years 3 months ago
A Typed Intermediate Language for Flow-Directed Compilation
We present a typed intermediate language λCIL for optimizing compilers for function-oriented and polymorphically typed programming languages (e.g., ML). The language λCIL is a ty...
J. B. Wells, Allyn Dimock, Robert Muller, Franklyn...
LFCS
2007
Springer
14 years 5 months ago
The Intensional Lambda Calculus
We introduce a natural deduction formulation for the Logic of Proofs, a refinement of modal logic S4 in which the assertion PA is replaced by [[s]]A whose intended reading is “s...
Sergei N. Artëmov, Eduardo Bonelli