-- JoseBacelarAlmeida - 19 Oct 2010

50 Recent Changes in TWiki Web retrieved at 17:35 (GMT)

See also: RSS feed, recent changes with 50, 100, 200, 500, 1000 topics, all changes

Program Semantics, Verification, and Construction

Overview.

The reliability of computing systems plays an essential role in modern society, where so many areas of human activity depend on technology. The deliverables of software projects may no longer be limited to code; the ability to produce certified code is now crucial. Code may be certified as being functionally correct, or as possessing certain execution properties (for instance, a program may be certified as not trying to access unauthorised resources).

The ability to certify software in this way requires a sound knowledge of the theory of programming languages and mathematical reasoning tools, as well as acquaintance with tool-assisted techniques. This course gives an overview of the theory of programming languages at an advanced level and then goes on to apply the theory to methods for obtaining correct, certified software.

Aims.

• to present in a systematic way a vast set of results in fundamental areas of Theoretical Computer Science, in particular Logic, Lambda-calculus, Type Theory and Programming Language Semantics, as well as the relationships between them;
• to introduce several rigorous approaches to the production of correct software, namely in:
  • Program Verification , the activity that aims to establish that a program effectively behaves according to its specification, or that its behaviour is characterised by a set of given properties;
  • in Mathematical Program Construction , a method for obtaining correct programs from specifications, strongly based on program calculation.

Lecturing Team.

The team consists of members of the Department of Informatics of the University of Minho and the Department of Computer Science of the University of Porto (Faculty of Science). All team members are working, and have worked actively in the past few years, on topics that are directly related to the subjects covered by this course, as detailed below.

• José Bacelar Almeida (DI-UM) has worked on the verification of security protocols, and has experience in using proof-assistants for program development.
• Sabine Broda (DCC-FCUP) has worked on Mathematical Logic, lambda-calculus, and Type Theory.
• Luís Damas (DCC-FCUP) has worked extensively on lambda-calculus and Type Theory; he is in fact responsible for the introduction of many of these subjects in Portugal.
• Mário Florido (DCC-FCUP) has worked on lambda-calculus, type systems, and program transformation.
• Maria J. Frade (DI-UM) has worked on lambda-calculus, type systems, and Proof Theory.
• Nelma Moreira (DCC-FCUP) has worked on Automata Theory, Proof Theory, and proof assistants.
• José N. Oliveira (DI-UM) has worked extensively on Formal Methods in Software Engineering and is in fact a pioneer of this area in Portugal. Recently he has become interested in the calculation-based approach to program construction.
• Jorge Sousa Pinto (DI-UM) has worked on Linear Logic, lambda-calculus, and functional program transformation.

• Education/MapiSCAM Web
• Create New Topic
• Index
• Search
• Changes
• Notifications
• Statistics
• Preferences

• Main Webs

•  DI
•  EL
•  Education
•  Events
•  JoseLuisSilva
•  Personal
•  Research

Education/MapiSCAM Web Preferences

The following settings are web preferences of the Education.MapiSCAM web. These preferences overwrite the site-level preferences in TWiki.TWikiPreferences and Main.TWikiPreferences, and can be overwritten by user preferences (your personal topic, eg: TWikiGuest in the Main web).

Web Parameters

• Set ANO_DEF = 1011

Web Preferences Settings

Preferences:

• Set SKIN=nat

• Set SKINSTYLE = Kubrick
• Set STYLEBORDER = thin
• Set STYLEBUTTONS = off
• Set STYLESIDEBAR = left
• Set STYLEVARIATION = none
• Set STYLESEARCHBOX = off

• Set PAGETITLE = MAP/i - Programming Paradigms

• Set NATWEBLOGO = MAP/i - Programming Paradigms
• Set WEBLOGOALT = Option IV: Source Code Analysis and Manipulation
• Set WEBLOGOURL = WebHome

• Set WEBCOPYRIGHT = Copyright © by the contributing authors. Ideas, requests, problems? Send feedback.

• List of topics of the Education/MapiSCAM web:
  • #Set WEBTOPICLIST = Changes | Index | Search | Go

• Web-specific background color: (Pick a lighter one of the StandardColors).
  • Set WEBBGCOLOR = #D0D0D0
  • Note: This setting is automatically configured when you create a web

• Image, URL and alternate tooltip text of web's logo.
  Note: Don't add your own local logos to the TWikiLogos topic; create your own logos topic instead.
  • #Set WEBLOGOIMG = /twiki/pub/Main/LocalLogos/um_eengP.jpg
  • #Set WEBLOGOURL = WebHome
  • #Set WEBLOGOALT = Option IV: Source Code Analysis and Manipulation

• List of topics of the TWiki.Education/MapiSCAM web:
  • Set WEBTITLE = MAP/i - Programming Paradigms

• List this web in the SiteMap:
  • If yes, Set SITEMAPLIST = on, and add the "what" and "use to..." description for the site map. Make sure to list only links that include the name of the web, e.g. Education/MapiSCAM.Topic links.
  • Set SITEMAPLIST = on
  • Set SITEMAPWHAT = Source Code Analysis and Manipulation (Mapi)
  • Set SITEMAPUSETO = Source Code Analysis and Manipulation (Mapi)

• Exclude web from a web="all" search: (Set to on for hidden webs)
  • Set NOSEARCHALL =

• Prevent automatic linking of WikiWords and acronyms (if set to on); link WikiWords (if empty); can be overwritten by web preferences:
  • #Set NOAUTOLINK =
  • Note: You can still use the [[...][...]] syntax to link topics if you disabled WikiWord linking. The <noautolink> ... </noautolink> syntax can be used to prevents links within a block of text.

• Default template for new topics for this web:
  • WebTopicEditTemplate? : Default template for new topics in this web. (Site-level is used if topic does not exist)
  • TWiki.WebTopicEditTemplate: Site-level default topic template

• Comma separated list of forms that can be attached to topics in this web. See TWikiForms for more information.
  • Set WEBFORMS =

• Users or groups who are not / are allowed to view / change / rename topics in the Education/MapiSCAM web: (See TWikiAccessControl). Remove the # to enable any of these settings. Remember that an empty setting is a valid setting; setting DENYWEBVIEW to nothing means that anyone can view the web.
  • #Set DENYWEBVIEW =
  • #Set ALLOWWEBVIEW =
  • #Set DENYWEBCHANGE =
  • Set ALLOWWEBCHANGE = TWikiAdminGroup, JoaoSaraiva
  • #Set DENYWEBRENAME =
  • #Set ALLOWWEBRENAME = TWikiAdminGroup

• Users or groups allowed to change or rename this WebPreferences topic: (e.g., TWikiAdminGroup)
  • #Set ALLOWTOPICCHANGE = TWikiAdminGroup
  • Set ALLOWTOPICRENAME = TWikiAdminGroup, JoaoSaraiva

• Web preferences that are not allowed to be overridden by user or topic preferences:
  • Set FINALPREFERENCES = NOSEARCHALL, ATTACHFILESIZELIMIT, WIKIWEBMASTER, WEBCOPYRIGHT, WEBTOPICLIST, DENYWEBVIEW, ALLOWWEBVIEW, DENYWEBCHANGE, ALLOWWEBCHANGE, DENYWEBRENAME, ALLOWWEBRENAME

Help on Preferences

• A preference setting is defined by:
  3 or 6 spaces * Set NAME = value
  Example:
  • Set WEBBGCOLOR = #FFFFC0
• A preferences setting can be disabled with a # sign. Remove the # sign to enable a local customisation. Example:
  
  • #Set DENYWEBCHANGE = UnknownUser
• Preferences are used as TWikiVariables by enclosing the name in percent signs. Example:
  • When you write variable %WEBBGCOLOR% , it gets expanded to #D0D0D0
• The sequential order of the preference settings is significant. Define preferences that use other preferences first, i.e. set WEBCOPYRIGHT before WIKIWEBMASTER since %WEBCOPYRIGHT% uses the %WIKIWEBMASTER% variable.
• You can introduce your own preferences variables and use them in your topics and templates.

Related Topics

• TWiki.TWikiPreferences, Main.TWikiPreferences - site-level preferences
• TWikiUsers - list of user topics. User topics can have optional user preferences
• TWikiVariables - list of common %VARIABLES%
• TWikiAccessControl - explains how to restrict access by users or groups

Tools

• Rename, move or delete this web:
  • Rename/move/delete web..., looking for references in all public webs - See also: ManagingWebs

Web Search

Search: \.*

Overview
Syllabus
Recommended Books?
Course Material?

Warning: Can't find topic Education/MapiSCAM.Topics1011

Create New Topic in Education/MapiSCAM Web

Once you have created the topic, consider adding links in related topics to the new topic so that there are more ways people can discover it.