Using Dependent Types to Port Type Systems to Low-Level Languages

TinkerType: a language for playing with formal systems

Journal of Functional Programming ◽

10.1017/s0956796802004550 ◽

2003 ◽

Vol 13 (2) ◽

pp. 295-316 ◽

Cited By ~ 14

Author(s):

MICHAEL Y. LEVIN ◽

BENJAMIN C. PIERCE

Keyword(s):

Operational Semantics ◽

Type Systems ◽

Dependent Types ◽

Inference Rules ◽

Safety Properties ◽

Formal Systems

TinkerType is a pragmatic framework for compact and modular description of formal systems (type systems, operational semantics, logics, etc.). A family of related systems is broken down into a set of clauses – individual inference rules – and a set of features controlling the inclusion of clauses in particular systems. Simple static checks are used to help maintain consistency of the generated systems. We present TinkerType and its implementation and describe its application to two substantial repositories of typed lambda-calculi. The first repository covers a broad range of typing features, including subtyping, polymorphism, type operators and kinding, computational effects, and dependent types. It describes both declarative and algorithmic aspects of the systems, and can be used with our tool, the TinkerType Assembler, to generate calculi either in the form of typeset collections of inference rules or as executable ML typecheckers. The second repository addresses a smaller collection of systems, and provides modularized proofs of basic safety properties.

Download Full-text

Dependent types ensure partial correctness of theorem provers

Journal of Functional Programming ◽

10.1017/s0956796803004921 ◽

2004 ◽

Vol 14 (1) ◽

pp. 3-19 ◽

Cited By ~ 11

Author(s):

ANDREW W. APPEL ◽

AMY P. FELTY

Keyword(s):

Programming Languages ◽

Decision Procedure ◽

Type Systems ◽

Theorem Prover ◽

Dependent Types ◽

Partial Correctness ◽

Proof Search ◽

Theorem Provers ◽

Proof Construction ◽

Correctness Of Programs

Static type systems in programming languages allow many errors to be detected at compile time that wouldn't be detected until runtime otherwise. Dependent types are more expressive than the type systems in most programming languages, so languages that have them should allow programmers to detect more errors earlier. In this paper, using the Twelf system, we show that dependent types in the logic programming setting can be used to ensure partial correctness of programs which implement theorem provers, and thus avoid runtime errors in proof search and proof construction. We present two examples: a tactic-style interactive theorem prover and a union-find decision procedure.

Download Full-text

Dependent Types for Low-Level Programming

Programming Languages and Systems - Lecture Notes in Computer Science ◽

10.1007/978-3-540-71316-6_35 ◽

2007 ◽

pp. 520-535 ◽

Cited By ~ 23

Author(s):

Jeremy Condit ◽

Matthew Harren ◽

Zachary Anderson ◽

David Gay ◽

George C. Necula

Keyword(s):

Dependent Types ◽

Low Level

Download Full-text

Strong normalisation in two Pure Pattern Type Systems

Mathematical Structures in Computer Science ◽

10.1017/s0960129508006749 ◽

2008 ◽

Vol 18 (3) ◽

pp. 431-465

Author(s):

BENJAMIN WACK ◽

CLÉMENT HOUTMANN

Keyword(s):

Pattern Matching ◽

Type Systems ◽

Expressive Power ◽

Positive Answer ◽

Point Of View ◽

Essential Property ◽

Dependent Types ◽

Pattern Type ◽

Logical Point

Pure Pattern Type Systems (P2TS) combine the frameworks and capabilities of rewriting and λ-calculus within a unified setting. Their type systems, which are adapted from Barendregt's λ-cube, are especially interesting from a logical point of view. Until now, strong normalisation, which is an essential property for logical soundness, has only been conjectured: in this paper, we give a positive answer for the simply-typed system and the dependently-typed system.The proof is based on a translation of terms and types fromP2TSinto the λ-calculus. First, we deal with untyped terms, ensuring that reductions are faithfully mimicked in the λ-calculus. For this, we rely on an original encoding of the pattern matching capability ofP2TSinto the System Fω.Then we show how to translate types: the expressive power of System Fω is needed in order to fully reproduce the original typing judgments ofP2TS. We prove that the encoding is correct with respect to reductions and typing, and we conclude with the strong normalisation of simply-typedP2TSterms. The strong normalisation with dependent types is in turn obtained by an intermediate translation into simply-typed terms.

Download Full-text

Tryptophan-Niacin Metabolism in Rat with Puromycin Aminonucleoside-Induced Nephrosis

International Journal for Vitamin and Nutrition Research ◽

10.1024/0300-9831.76.1.28 ◽

2006 ◽

Vol 76 (1) ◽

pp. 28-33 ◽

Cited By ~ 7

Author(s):

Yukari Egashira ◽

Shin Nagaki ◽

Hiroo Sanada

Keyword(s):

Body Weight ◽

Urinary Excretion ◽

Enzyme Activities ◽

Treated Group ◽

Control Group ◽

Puromycin Aminonucleoside ◽

Low Level ◽

Key Enzyme

We investigated the change of tryptophan-niacin metabolism in rats with puromycin aminonucleoside PAN-induced nephrosis, the mechanisms responsible for their change of urinary excretion of nicotinamide and its metabolites, and the role of the kidney in tryptophan-niacin conversion. PAN-treated rats were intraperitoneally injected once with a 1.0% (w/v) solution of PAN at a dose of 100 mg/kg body weight. The collection of 24-hour urine was conducted 8 days after PAN injection. Daily urinary excretion of nicotinamide and its metabolites, liver and blood NAD, and key enzyme activities of tryptophan-niacin metabolism were determined. In PAN-treated rats, the sum of urinary excretion of nicotinamide and its metabolites was significantly lower compared with controls. The kidneyα-amino-β-carboxymuconate-ε-semialdehyde decarboxylase (ACMSD) activity in the PAN-treated group was significantly decreased by 50%, compared with the control group. Although kidney ACMSD activity was reduced, the conversion of tryptophan to niacin tended to be lower in the PAN-treated rats. A decrease in urinary excretion of niacin and the conversion of tryptophan to niacin in nephrotic rats may contribute to a low level of blood tryptophan. The role of kidney ACMSD activity may be minimal concerning tryptophan-niacin conversion under this experimental condition.

Download Full-text