Langages Fonctionnels - Functional languages
GROUPES - GROUPS
<http://www.dcs.gla.ac.uk/fp/>
<http://www.cs.chalmers.se/ComputingScience/Research/Functional/>
Central to the current work within the programming logic group is the idea of a logical framework for programming ; i.e. a unified theory of formal systems in which many different logics can be conveniently expressed. In particular, much of our work is based on Martin-Löf's theory of types, which provides such a framework.
<http://www.cs.chalmers.se/Cs/Research/Logic/>
University of Nottingham
<http://www.cs.nott.ac.uk/Research/lap/>
PAGES WEB
Curry is a universal programming language aiming to amalgamate the most important declarative programming paradigms, namely functional programming and logic programming. Moreover, it also covers the most important operational principles developed in the area of integrated functional logic languages: "residuation" and "narrowing"
<http://www-i2.informatik.rwth-aachen.de/~hanus/curry/index.html>
<http://www-i2.informatik.rwth-aachen.de/Forschung/FP/Haskell/>
<http://www.erlang.org/>
is a robust, fully-featured, optimising compiler for Haskell 98, GHC compiles Haskell to either native code or C.
<http://research.microsoft.com/users/t-simonm/ghc/>
This binary distribution doesn't work on RedHat 6.0.
<http://www.netlib.org/pvm3/>
Haskell is a general purpose, purely functional programming language. Haskell compilers are freely available for almost any computer.
<http://www.haskell.org/>
a Haskell interpreter and programming environment for developing cool Haskell programs. Sources and binaries are freely available by anonymous FTP and on the World-Wide Web. The release and supporting documents can be
downloaded from the Hugs home page.
<http://haskell.systemsz.cs.yale.edu/hugs/>
Hotter than Haskell
Cayenne is a simple(?) functional language with a powerful type system. The basic types are functions, products, and sums. Functions and products use dependent types to gain additional power.
<http://www.cs.chalmers.se/~augustss/cayenne/index.html>
is a system for incrementally developing proofs and programs. Agda is also a functional language with dependent types. This language is very similar to cayenne and agda is intended to be a (almost) full implementation of it in the future.
Alfa is a successor of the proof editor Alf with a graphical user interface.
<http://www.cs.chalmers.se/~catarina/agda/>
ALF is a language which combines functional and logic programming techniques. The foundation of ALF is Horn clause logic with equality which consists of predicates and Horn clauses for logic programming, and functions and equations for functional programming. Since ALF is a genuine integration of both programming paradigms, any functional expression can be used in a goal literal and arbitrary predicates can occur in conditions of equations. The operational semantics of ALF is based on the resolution rule to solve literals and narrowing to evaluate functional expressions.
<http://www-i2.informatik.rwth-aachen.de/~hanus/systems/ALF.html>
A proof-assistant is a computer program with which a user can construct completely formal mathematical proofs in some kind of logical system. In contrast to a theorem prover, a proof-assistant cannot find proofs on its own.
<http://www.cs.kun.nl/~janz/yarrow/>
developed at Carnegie Mellon by the SCandAL project
<http://www.cs.cmu.edu/~scandal/nesl.html>
<http://www.mozart-oz.org/>
University of St Andrews
<http://www-fp.dcs.st-and.ac.uk/>
CLEAN is a state-of-the-art, pure and lazy functional programming language specially designed to make the development of real world applications possible.
<http://www.cs.kun.nl:80/~clean/>
The United Functions and Objects project has developed a programming language which unites functional and Object Oriented Programming techniques.
<http://www.cs.man.ac.uk/arch/projects/ufo.html>
he HOL system is a powerful and widely used computer program for constructing formal specifications and proofs in higher order logic. The system is used in both industry and academia to support formal reasoning in many different areas, including hardware design and verification, reasoning about security, proofs about real-time systems, semantics of hardware description languages, compiler verification, program correctness, modelling concurrency, and program refinement. HOL is also used as an open platform for general theorem-proving research.
<http://www.cs.bell-labs.com/~wadler/realworld/hol.html>
a simulator for the parallel execution of Glasgow Parallel Haskell (GPH) programs. Haskell is a non-strict, purely-functional programming language. GPH extends Haskell with annotations for sequential (seq) and parallel (par) composition.
<http://www.dcs.glasgow.ac.uk/fp/software/gransim/>
Cayenne is a simple(?) functional language with a powerful type system. The basic types are functions, products, and sums. Functions and products use dependent types to gain additional power.
<http://www.cs.chalmers.se/~augustss/cayenne/>
ASSOCIATIONS
This is the web site is dedicated to the preservation, promotion and development of the TRAC programming language.
<http://www.trac-language.com/>
Haskell is a general purpose, purely functional programming language. Haskell compilers are freely available for almost any computer.
<http://www.haskell.org/ghc/>
PAGES PERSONNELLES - HOME PAGES
<http://www.dcs.gla.ac.uk/~andy/>
Chalmers University of Technology
<http://www.md.chalmers.se/~rjmh/>
Computer Science Department, Yale University
Functional Programming Computer Music Jazz
<http://www.cs.yale.edu/~hudak-paul.html>
<http://www.base.com/gordoni/>
<http://research.microsoft.com/Users/simonpj/#aspects>
SOURCES
<ftp://ftp.dcs.glasgow.ac.uk/pub/haskell/gofer/>
<http://www.haskell.org/hugs/>
GHC-Current is basically a recent snapshot of the source tree, guaranteed to be taken at a point when the sources build successfully (but don't necessarily work!).
<http://research.microsoft.com/users/t-simonm/ghc/download_ghc_current.html>
<ftp://ftp.cs.chalmers.se/pub/haskell/chalmers/0.9999.3/>
For Cayenne to work you need hbc and lmlc which can be found at
ftp.cs.chalmers.se/pub/haskell/chalmers
<ftp://ftp.cs.chalmers.se/users/cs/augustss/cayenne.tgz>
JAVA
Klaus Havelund
The Java PathFinder, JPF, is a translator from Java to Promela, the programming language of the SPIN model checker. The purpose is to establish a framework for verification and debugging of Java programs using model checking. The system detects deadlocks and violations of assertions stated by the programmer.
<http://www.cs.bell-labs.com/~wadler/realworld/javapathfinder.html>
A substantial companion to Java
Pizza is an extension of Java with three important new features. Parametric polymorphism. First-class functions. Class cases and pattern matching.
Pizza compiles programs to ordinary Java Byte Code, and interfaces with existing Java code, retaining the broad compatibility of Java.
<http://www.cis.unisa.edu.au/~pizza/>
DOCUMENTS - PAPERS
Philip Wadler
<http://www.cs.bell-labs.com/~wadler/topics/monads.html>
Philip Wadler
<http://www.cs.bell-labs.com/~wadler/topics/linear-logic.html>
<http://www.dcs.gla.ac.uk/fp/authors/Simon_Peyton_Jones/>
Jean-Louis Krivine
<http://www.pps.jussieu.fr/~krivine/articles/interprt.pdf>
RÉSUMÉS - ABSTRACTS
KIV is an interactive theorem prover with a user definable object logic.
<http://www.cs.bell-labs.com/~wadler/realworld/kiv.html>
John Hughes
<http://www.md.chalmers.se/~rjmh/Papers/whyfp.html>
JOURNAUX - LETTERS
<http://www.dcs.gla.ac.uk/jfp/>
Jean-Paul Baquiast et Christophe Jacquemin
Les automates intelligents robotique, vie artificielle, réalité virtuelle
<http://www.admiroutes.asso.fr/larevue/2002/27/edito.htm>
TUTORIELS - TUTORIALS - TUTORS
The mission of the Sisal Language Project is to develop high-performance functional compilers and runtime systems to simplify the process of writing scientific programs on parallel supercomputers and to help programmers develop functional scientific applications.
<http://jarl.cs.uop.edu/cop/cs/faculty/joseph/SisalTutorial/>
<http://www.cit.gu.edu.au/~arock/entre/entre.html>
Jean Goubault-Larrecq Le 02 août 1999
<http://www.dyade.fr/fr/actions/VIP/jgl/MMFAI/lambdaidx.html>
Jean Goubault-Larrecq
<http://www.lsv.ens-cachan.fr/~goubault/machinesidx.html>
MANUELS - MANUALS
Alfa is a WYSIWYG proof editor. It allows you to, interactively and incrementally, define theories (axioms and inference rules), formulate theorems and construct proofs of the theorems. All steps in the proof construction are immediately checked by the system and no erroneous proofs can be constructed. The logical framework used is Agda
<http://www.cs.chalmers.se/~hallgren/Alfa/userguide.html>
<http://haskell.org/bookshelf/>
QUESTIONS - FAQ
Edited by Graham Hutton, University of Nottingham
<http://www.cs.nott.ac.uk/Department/Staff/gmh/faq.html>
<http://www.cis.ohio-state.edu/hypertext/faq/usenet/func-lang-faq/faq.html>
GROUPES DE DISCUSSION - NEWS
<news:comp.lang.functional>
LIENS - LINKS
<http://www-i2.informatik.rwth-aachen.de/~hanus/FLP/implementations.html>
<http://compiler.kaist.ac.kr/~khchoi/fp.html>
<http://www.studyweb.com/computers/program/functional.htm>
Here is a list of functional programs applied to real-world tasks. The main criterion for being real-world is that the program was written primarily to perform some task, not primarily to experiment with functional programming.
<http://www.cs.bell-labs.com/~wadler/realworld/index.html>
<http://www.cs.cmu.edu/~mleone/language-research.html>