431:
199:, an approach to representing syntax that maps object-level bindings to programming language bindings. Programmers in λProlog need not deal with bound variable names: instead various declarative devices are available to deal with binder scopes and their instantiations.
548:
558:
472:
207:
Since 1986, λProlog has received numerous implementations. As of 2023, the language and its implementations are still actively being developed.
210:
The Abella theorem prover has been designed to provide an interactive environment for proving theorems about the declarative core of λProlog.
507:
239:
115:
335:
553:
339:
465:
195:
244:
264:
158:
170:
458:
190:
361:
186:
438:
33:
227:
166:
492:
System
Description: Teyjus - A Compiler and Abstract Machine Based Implementation of lambda Prolog
517:
182:
162:
430:
377:
is currently the oldest implementation still being maintained. This compiler project is led by
219:
408:
503:
38:
321:
495:
356:
90:
73:
529:
234:
45:
311:
442:
343:
178:
542:
223:
291:
193:
gives λProlog the basic supports needed to capture the λ-tree syntax approach to
388:
63:
418:
prover can be used to prove theorems about λProlog programs and specifications.
499:
17:
299:
378:
295:
307:
400:
174:
132:
404:
392:
327:
317:
396:
384:
78:
415:
374:
265:"FAQ: What implementations of lambda Prolog are available?"
446:
304:, published by Cambridge University Press in June 2012.
403:
that appeared LPAR 2015. ELPI is also available as a
312:
138:
126:
113:
85:
72:
62:
54:
44:
32:
395:. It is implemented in OCaml and is available
466:
181:used to justify the foundations of λProlog.
177:are derived from the higher-order hereditary
8:
27:
490:Nadathur, Gopalan; Dustin Mitchell (1999).
381:and various of his colleagues and students.
494:. LNAI. Vol. 1632. pp. 287–291.
473:
459:
26:
334:(163 pages, French). It is available as
482:
385:ELPI: an Embeddable λProlog Interpreter
256:
525:
515:
7:
427:
425:
332:Lambda-Prolog de A à Z... ou presque
240:Comparison of Prolog implementations
364:at the Software Preservation Group.
301:Programming with higher-order logic
549:Prolog programming language family
310:has written in a 1997 tutorial on
25:
322:Program Analysis in lambda Prolog
559:Programming language topic stubs
429:
50:Dale Miller and Gopalan Nadathur
399:. The system is described in a
220:Curry's paradox#Lambda calculus
324:for the 1998 PLILP Conference.
1:
226:problems caused by combining
445:. You can help Knowledge by
196:higher-order abstract syntax
375:The Teyjus λProlog compiler
245:Prolog syntax and semantics
183:Higher-order quantification
575:
424:
320:has written a tutorial on
159:logic programming language
79:GNU General Public License
554:Logic in computer science
143:
131:
121:
500:10.1007/3-540-48660-7_25
269:www.lix.polytechnique.fr
191:higher-order unification
171:higher-order programming
173:. These extensions to
441:-related article is a
393:Claudio Sacerdoti Coen
387:has been developed by
298:have written the book
407:: see Enrico Tassi's
228:(propositional) logic
439:programming-language
187:simply typed λ-terms
286:Tutorials and texts
167:modular programming
55:First appeared
29:
163:polymorphic typing
509:978-3-540-66222-8
454:
453:
148:
147:
64:Typing discipline
39:Logic programming
16:(Redirected from
566:
534:
533:
527:
523:
521:
513:
487:
475:
468:
461:
433:
426:
379:Gopalan Nadathur
357:λProlog homepage
296:Gopalan Nadathur
279:
278:
276:
275:
261:
109:
106:
104:
102:
100:
98:
96:
94:
92:
46:Designed by
30:
21:
574:
573:
569:
568:
567:
565:
564:
563:
539:
538:
537:
524:
514:
510:
489:
488:
484:
480:
479:
422:
411:on this plugin.
371:
369:Implementations
353:
288:
283:
282:
273:
271:
263:
262:
258:
253:
235:lambda calculus
216:
205:
179:Harrop formulas
153:, also written
116:implementations
89:
23:
22:
15:
12:
11:
5:
572:
570:
562:
561:
556:
551:
541:
540:
536:
535:
526:|journal=
508:
481:
478:
477:
470:
463:
455:
452:
451:
434:
420:
419:
412:
382:
370:
367:
366:
365:
359:
352:
351:External links
349:
348:
347:
328:Olivier Ridoux
325:
315:
305:
287:
284:
281:
280:
255:
254:
252:
249:
248:
247:
242:
237:
222:— about
215:
212:
204:
201:
146:
145:
141:
140:
136:
135:
129:
128:
124:
123:
119:
118:
111:
110:
95:.polytechnique
87:
83:
82:
76:
70:
69:
68:strongly typed
66:
60:
59:
56:
52:
51:
48:
42:
41:
36:
24:
14:
13:
10:
9:
6:
4:
3:
2:
571:
560:
557:
555:
552:
550:
547:
546:
544:
531:
519:
511:
505:
501:
497:
493:
486:
483:
476:
471:
469:
464:
462:
457:
456:
450:
448:
444:
440:
435:
432:
428:
423:
417:
413:
410:
406:
402:
398:
394:
390:
386:
383:
380:
376:
373:
372:
368:
363:
360:
358:
355:
354:
350:
345:
341:
337:
333:
329:
326:
323:
319:
316:
313:
309:
306:
303:
302:
297:
293:
290:
289:
285:
270:
266:
260:
257:
250:
246:
243:
241:
238:
236:
233:
229:
225:
224:inconsistency
221:
218:
217:
213:
211:
208:
202:
200:
198:
197:
192:
188:
184:
180:
176:
172:
168:
164:
160:
156:
155:lambda Prolog
152:
142:
137:
134:
130:
127:Influenced by
125:
120:
117:
112:
108:
88:
84:
80:
77:
75:
71:
67:
65:
61:
57:
53:
49:
47:
43:
40:
37:
35:
31:
19:
491:
485:
447:expanding it
436:
421:
389:Enrico Tassi
331:
330:has written
300:
272:. Retrieved
268:
259:
231:
209:
206:
194:
154:
150:
149:
122:Teyjus, ELPI
18:LambdaProlog
318:John Hannan
292:Dale Miller
543:Categories
405:Coq plugin
336:PostScript
274:2019-12-16
251:References
161:featuring
139:Influenced
528:ignored (
518:cite book
308:Amy Felty
409:tutorial
214:See also
105:/lProlog
34:Paradigm
232:untyped
203:History
157:, is a
151:λProlog
103:.Miller
86:Website
74:License
28:λProlog
506:
416:Abella
397:online
342:, and
189:, and
175:Prolog
169:, and
133:Prolog
114:Major
437:This
401:paper
362:Entry
144:Makam
101:/Dale
99:/Labo
530:help
504:ISBN
443:stub
414:The
391:and
344:html
294:and
230:and
93:.lix
58:1987
496:doi
340:PDF
97:.fr
91:www
545::
522::
520:}}
516:{{
502:.
338:,
267:.
185:,
165:,
81:v3
532:)
512:.
498::
474:e
467:t
460:v
449:.
346:.
314:.
277:.
107:/
20:)
Text is available under the Creative Commons Attribution-ShareAlike License. Additional terms may apply.