Share This
table started by
warren for the Proofs are Programs Base
There is no user-contributed description yet.
Add More Topics
Save this view to a base, or just for yourself.
23 Key Application topics matching:
Filter this Collection|
|
|||
|---|---|---|---|
| x name | x image | x How it applied the concept | x article |
| x ML | ML, short for ‘metalanguage’ was the first programming language to make use of the Hindley-Milner type inference algorithm. |
ML is a general-purpose functional programming language developed by Robin Milner and others in the late 1970s at the University of Edinburgh, whose syntax is inspired by ISWIM. Historically, ML stands for metalanguage: it was conceived to develop...
|
|
| x Standard ML |
Standard ML (SML) is a general-purpose, modular, functional programming language with compile-time type checking and type inference. It is popular among compiler writers and programming language researchers, as well as in the development of theorem...
|
||
| x Objective Caml |
|
Objective Caml, or OCaml (pronounced /oʊˈkæməl/ oh-KAM-əl) is the main implementation of the Caml programming language, created by Xavier Leroy, Jérôme Vouillon, Damien Doligez, Didier Rémy and others in 1996. OCaml is a free open source project...
|
|
| x Haskell |
|
The Haskell programming languages continues to explore the power of theorem proving in its type language through the development of type classes. |
Haskell (pronounced [ˈhæskəl]) is a standardized, general-purpose purely functional programming language, with non-strict semantics and strong static typing. It is named after logician Haskell Curry.
Following the release of Miranda by Research...
|
| x NuPRL | Early theorem prover which utilized correspondence between proofs and programs. |
NuPRL is a higher-order proof development system developed at Cornell University. It was founded by Joseph L. Bates and Robert L. Constable in 1979 and, since then, many have contributed to the development of NuPRL.
|
|
| x Kleisli |
Kleisli is a database language for biomedical data (implemented in Standard ML).
|
||
| x XDuce |
XDuce ("tranceduce") is an XML transformation language.
|
||
| x Pi-calculus |
In theoretical computer science, the π-calculus is a process calculus originally developed by Robin Milner, Joachim Parrow and David Walker as a continuation of work on the process calculus CCS (Calculus of Communicating Systems). The aim of the π...
|
||
| x Join-calculus |
The join-calculus is a process calculus developed at INRIA. The join-calculus was developed to provide a formal basis for the design of distributed programming languages, and therefore intentionally avoids communications constructs found in other...
|
||
| x HOL theorem prover | Hewlett-Packard applied the HOL (Higher-Order Logic) theorem prover as part of an effort to verify that caching protocol’s in its Runway multiprocessor bus did not deadlock. This approach uncovered errors that had not been revealed by several months of simulation. |
HOL (Higher Order Logic) denotes a family of interactive theorem proving systems sharing similar logics and implementation strategies. Systems in this family follow the LCF approach as they are implemented as a library in some programming language....
|
|
| x LCF theorem prover | ML/LCF exploited two central features of functional languages, higher-order functions and types. A proof tactic is a function taking a goal formula to be proved and returning a list of subgoals paired with a justification. A justification, in turn, is a function from proofs of the subgoals to a proof of the goal. A tactical is a function that combined small tactics into larger tactics. The type system was a great boon in managing the resulting nesting of functions that return functions that accept functions. |
LCF (Logic for Computable Functions) is an interactive automated theorem prover developed at the universities of Edinburgh and Stanford by Robin Milner and others. LCF introduced the general-purpose programming language ML to allow users to write...
|
|
| x Isabelle theorem prover |
The Isabelle theorem prover is an interactive theorem proving framework, a successor of the Higher Order Logic (HOL) theorem prover. It is an LCF-style theorem prover (written in Standard ML), so it is based on a small logical core guaranteeing...
|
||
| x Coq |
|
In computer science, Coq is a proof application. It allows the expression of mathematical assertions, mechanically checks proofs of these assertions, helps to find formal proofs, and extracts a certified program from the constructive proof of its...
|
|
| x Miranda |
|
Miranda is a non-strict purely functional programming language designed by David Turner as a successor to his earlier programming languages SASL and KRC, using some concepts from ML and Hope. It was produced by Research Software Ltd. of England ...
|
|
| x Twelf |
Twelf is an implementation of the logical framework LF. It is used for logic programming and for the formalization of programming language theory.
At its simplest, a Twelf program (called a "signature") is a collection of declarations of type...
|
||
| x Functional programming | In many ways, the entire discipline of functional programming is an outcome of Church's lambda calculus and the Curry-Howard correspondence between proofs and programs. Church and Curry lived to see their abstract theories have an impact on practical programming languages. They were guests of honor at the 1982 conference on Lisp and Functional Programming, both highly bemused by what had been done with their work. |
In computer science, functional programming is a programming paradigm that treats computation as the evaluation of mathematical functions and avoids state and mutable data. It emphasizes the application of functions, in contrast to the imperative...
|
|
| x Proof-Carrying Code | Proof-carrying code leverages the Curry-Howard correspondence as a means to validate programs for security and operational safety. The first application was to the Berkely Packet Filter, or BPF, a small interpreted language for packet filters built-in to the kernel of Berkeley Unix which enforces the safety policy by run-time checks. |
Proof-carrying code (PCC) is a software mechanism that allows a host system to verify properties about an application via a formal proof that accompanies the application's executable code. The host system can quickly verify the validity of the proof...
|
|
| x Typed Assembly Language |
In computer science, a typed assembly language (TAL) is an assembly language that is extended to include a method of annotating the datatype of each value that is manipulated by the code. These annotations can then be used by a program (type checker...
|
||
| x Calculus of constructions |
The calculus of constructions (CoC) is a formal language in which both computer programs and mathematical proofs can be expressed. This language forms the basis of theory behind the Coq proof assistant, which implements the derivative calculus of...
|
||
| x ISWIM |
ISWIM is an abstract computer programming language (or a family of programming languages) devised by Peter J. Landin and first described in his article, The Next 700 Programming Languages, published in the Communications of the ACM in 1966. The...
|
||
| x Lisp |
|
McCarthy's lisp was the first programming language to embrace the lambda calculus as its key computing paradigm. |
Lisp (or LISP) is a family of computer programming languages with a long history and a distinctive, fully parenthesized syntax. Originally specified in 1958, Lisp is the second-oldest high-level programming language in widespread use today; only...
|
| x Lambda cube |
In mathematical logic and type theory, the λ-cube is a framework for exploring the axes of refinement in Coquand's calculus of constructions, starting from the simply typed lambda calculus as the vertex of a cube placed at the origin, and the...
|
||
| x Java |
|
Generic types in Java were developed by Odersky, Wadler and others to bring the power of parametric polymorphism to this popular programming language. |
Java refers to a number of computer software products and specifications from Sun Microsystems that together provide a system for developing application software and deploying it in a cross-platform environment. Java is used in a wide variety of...
|
