@hackage pisigma0.2

A dependently typed core language

Categories
- Development
- Language
License
BSD-3-Clause
Maintainer
Thorsten Altenkirch <txa@cs.nott.ac.uk>, Andres Loeh <kspisigma@andres-loeh.de>
Links
- Documentation
- No source repository
Versions
- 0.2.1 Wed, 18 May 2011
- 0.2 Mon, 31 May 2010
- 0.1.0.3 Tue, 1 Dec 2009
- 0.1.0.2 Sun, 11 Oct 2009
- 0.1.0.1 Sat, 10 Oct 2009

Installation
In your cabal file:
Dependencies (11)
- array >=0.2 && <0.4
- base >=4.0 && <5.0
- bytestring >=0.9 && <1.0
- containers >=0.2 && <0.4
- mtl >=1.1 && <1.2
- parsec >=3.0 && <4.0
Dependents (1)
@hackage/acme-everything

Package Flags

debug

(off by default)

Enable debug support

PiSigma is a small dependently typed language with only very few constructs: Type:Type, Pi-types, Sigma-types, enumerations and a general meachanism for mutual recursion for types and values controlled by lifted types. It is intended as a core language for dependently typed languages like Agda. It has been described in the paper emPiSigma: Dependent Types Without the Sugar/em which has appeared in the proceedings of FLOPS 2010.

@hackage pisigma0.2

Categories

License

Maintainer

Links

Versions

Installation

Dependencies (11)

Dependents (1)

Package Flags