## User login## Navigation |
## Logic/Declarative## Milawa: 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 | 12718 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 | 14705 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 | 10121 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 | 13565 reads
## SequenceL - declarative computation on nonscalarsI recently came across the language 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 By Allan McInnes at 2009-10-11 21:34 | Functional | Logic/Declarative | 13 comments | other blogs | 11394 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 | 11527 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 | 132806 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 | 7190 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 | 14256 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: - It extends the language, so that clauses can talk about not just satisfaction of predicates, but also of an agent desiring to bring about a predicate, and desiring to find out whether a predicate is true; and to distinguish between normal goals and special goals relevant to the BDI model (Belief-Desire-Intention model);
- It amends the resolution engine to support what Rao calls
*reactive concurrency*, where agents form plans via a process resembling SLD-resolution, but plans are formed or abandoned on the basis of agent-internal reactions called triggering events.
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

2 days 5 hours ago

1 week 1 day ago

1 week 5 days ago

2 weeks 5 days ago

3 weeks 11 hours ago

3 weeks 11 hours ago

3 weeks 15 hours ago

4 weeks 11 hours ago

4 weeks 4 days ago

4 weeks 5 days ago