User loginNavigation |
Logic/DeclarativeMilawa: A Self-Verifying Theorem Prover for an ACL2-Like LogicMilawa: A Self-Verifying Theorem Prover for an ACL2-Like Logic
This might help inform discussions of the relationship between the de Bruijn criterion (the "social process" of mathematics) and formal verification. I think it also serves as an interesting signpost on the road forward: it's one thing to say that starting with a de Bruijn core and evolving a more powerful prover is possible in principle; it's another thing for it to actually have been done. The author's thesis defense slides provide a nice, quick overview. By Paul Snively at 2010-05-29 17:49 | DSL | Functional | Implementation | Lambda Calculus | Logic/Declarative | Semantics | 11 comments | other blogs | 13529 reads
A Lambda Calculus for Real AnalysisA Lambda Calculus for Real Analysis
Paul Taylor is deadly serious about the intersection of logic, mathematics, and computation. I came across this after beating my head against Probability Theory: The Logic of Science and Axiomatic Theory of Economics over the weekend, realizing that my math just wasn't up to the tasks, and doing a Google search for "constructive real analysis." "Real analysis" because it was obvious that that was what both of the aforementioned texts were relying on; "constructive" because I'd really like to develop proofs in Coq/extract working code from them. This paper was on the second page of results. Paul's name was familiar (and not just because I share it with him); he translated Jean-Yves Girard's regrettably out-of-print Proofs and Types to English and maintains a very popular set of tools for typesetting commutative diagrams using LaTeX. By Paul Snively at 2010-02-16 22:00 | Category Theory | Functional | Lambda Calculus | Logic/Declarative | Meta-Programming | Semantics | Type Theory | 9 comments | other blogs | 15587 reads
Certified Programming With Dependent Types Goes BetaCertified Programming With Dependent Types From the introduction:
This is the best Coq tutorial that I know of, partially for being comprehensive, and partially for taking a very different tack than most with Adam's emphasis on proof automation using Coq's Ltac tactic language. It provides an invaluable education toward understanding what's going on either in LambdaTamer or Ynot, both of which are important projects in their own rights. Please note that Adam is explicitly requesting feedback on this work. By Paul Snively at 2010-01-09 16:56 | Functional | Lambda Calculus | Logic/Declarative | Misc Books | Semantics | Teaching & Learning | Type Theory | 6 comments | other blogs | 10746 reads
ActorScript(TM): Industrial strength integration of local and nonlocal concurrency for Client-cloud Computing
ActorScript(TM): Industrial strength integration of local and nonlocal concurrency for Client-cloud Computing
by Carl Hewitt, 2009.
ActorScript is based on a mathematical model of computation that treats “Actors†as the universal primitives of concurrent digital computation [Hewitt, Bishop, and Steiger 1973; Hewitt 1977]. Actors been used both as a framework for a theoretical understanding of concurrency, and as the theoretical basis for several practical implementations of concurrent systems.I hope I do not need to introduce Carl Hewitt or his Actor model. This paper is a modern attempt to expose that model via a practical PL. By Andris Birkmanis at 2009-12-14 13:47 | Logic/Declarative | Object-Functional | 8 comments | other blogs | 14987 reads
SequenceL - declarative computation on nonscalarsI recently came across the language SequenceL, which it seems NASA is using in some of its human spaceflight programs. SequenceL is described as a high-level language for declarative computation on nonscalars. One of the key features of the language appears to be the avoidance of the need to explicitly specify recursive or iterative operations. For example, given the function definition Search(scalar Target, tuple [Subscript, Word]) = Subscript when Word = Target which applies to tuples, the programmer can apply the function directly to lists of tuples without any need to specify how that application will be performed, e.g. search(fox,[[1,dog],[2,cat],[3,fox],[4,parrot]]) → 3 search(rabbit,[[1,dog],[2,cat],[3,fox],[4,parrot]]) → [] The language designers (Daniel Cooke and J. Nelson Rushton) claim that this kind of thing leads to more concise and readable code, and a more direct representation of a specification. Unfortunately, the SequenceL website appears to be inaccessible at the moment. However, Daniel Cooke's site includes links to a number of papers and talks that describe SequenceL. In particular, the paper Normalize, Transpose, and Distribute: An Automatic Approach for Handling Nonscalars provides a detailed description of the "Consume-Simplify-Produce/Normalize-Transpose" approach that is embodied by SequenceL. There's also an overview of SequenceL available through CiteSeer. By Allan McInnes at 2009-10-11 21:34 | Functional | Logic/Declarative | 13 comments | other blogs | 12079 reads
Verified Programming in GuruVerified Programming in Guru is a tutorial introduction to Guru:
In comparison to Coq:
The tutorial is worth a read to anybody new to this style of programming as it is one of the most gentle introductions to dependent types and automated program verification that I've seen. By James Iry at 2009-08-05 02:59 | Logic/Declarative | Meta-Programming | Teaching & Learning | Type Theory | 4 comments | other blogs | 13294 reads
Creator of Qi Calls It QuitsIn a Qilang mailing list email Marker Tarver, creator of Qi, says
By James Iry at 2009-08-02 12:25 | Functional | Logic/Declarative | 8 comments | other blogs | 181411 reads
D is for Domain and DeclarativeThe list of accepted papers is out for the IFIP Working Conference on Domain Specific Languages. Happily for me, the program reveals much interest in languages for reasoning, decision making, and search. Even among people who are not my coauthors. :) Declarative programming tends to attract skepticism because it has the reputation of poor and hard-to-control performance. The approach of DSL embedding appears to ameliorate this problem, and the success of SAT solvers appears to chip away at this reputation. Meanwhile, the call for papers is out for Principles and Practice of Declarative Programming 2009, which has a venerable program committee. The submission deadline is May 7. By Chung-chieh Shan at 2009-03-24 20:50 | DSL | Logic/Declarative | 5 comments | other blogs | 7680 reads
Qi IIQi II has been released. Qi is a functional programming language built on top of Common Lisp. It has an optional static type system based on sequent calculus and a general focus on logic based programming. For version II, see the what's new page. Rule closures in particular look very interesting.
Also with this release is a new book: Funcitonal Programming in Qi. Earlier versions of Qi have been mentioned on LtU here and here. By James Iry at 2008-11-29 23:20 | Functional | Logic/Declarative | 4 comments | other blogs | 14974 reads
AgentSpeak(L): programming with beliefs, desires and intentionsAnand S. Rao (1996). AgentSpeak(L): BDI Agents speak out in a logical computable language. Rao's AgentSpeak(L) is a Prolog-like resolution-based language, but which is extended to support agent-based programming in several ways, most importantly:
Rao and Georgeff's work on BDI agents and procedural reasoning together constitutes one of the most important contributions to the theory of agents in AI, a topic which hasn't been discussed much here on LtU, but was raised in the Agent Oriented Programming story. |
Browse archives
Active forum topics
|
Recent comments
11 weeks 1 day ago
15 weeks 3 days ago
17 weeks 18 hours ago
17 weeks 18 hours ago
19 weeks 5 days ago
24 weeks 2 days ago
24 weeks 3 days ago
24 weeks 6 days ago
24 weeks 6 days ago
27 weeks 4 days ago