Functional Programming With Logical Frameworks: The Delphin Project - Softcover

Poswolsky, Adam Brett

Softcover

ISBN 10: 1440474923 ISBN 13: 9781440474927

Publisher: CreateSpace Independent Publishing Platform, 2008

Synopsis

Logical frameworks are languages used to represent information. In this dissertation we present Delphin (http://www.delphin.logosphere.org/), which is a functional programming language with a logical framework supporting both higher-order abstract syntax and dependent types. Higher-order abstract syntax, or HOAS, refers to the technique of representing variables of an object language using variables of a metalanguage, which leads to more concise and elegant encodings than first-order alternatives. Dependent types allow one to represent complex data (e.g. derivations) and enforce more properties of programs than possible using only simple types.Delphin is not only a useful programming language but also a useful system for formalizing proofs as total functions express proofs that the input entails the output.We motivate our system with examples of translating derivations between logics and converting between higher-order and first-order representations of data.

Edition details

• Publisher: CreateSpace Independent Publishing Platform
• Publication date: 2008
• Language: English
• ISBN 10: 1440474923
• ISBN 13: 9781440474927
• Binding: Paperback
• Number of pages: 484